pub proof fn lemma_frame_preserving_opt<RA: ResourceAlgebra>(a: RA, b: RA)Expand description
requires
frame_preserving_update_opt::<RA>(a, b),frame_preserving_update::<Option<RA>>(Some(a), Some(b)),