Skip to main content

lemma_incl_opt_rev

vstd::resource::option

Function lemma_incl_opt_rev 

Source 
pub proof fn lemma_incl_opt_rev<RA: ResourceAlgebra>(a: RA, b: RA)
Expand description
requires
incl::<Option<RA>>(Some(a), Some(b)),
ensures
incl::<RA>(a, b) || a == b,