Skip to main content

lemma_incl_opt

vstd::resource::option

Function lemma_incl_opt 

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