Function lemma_frame_preserving_update_nondeterministic_opt

pub proof fn lemma_frame_preserving_update_nondeterministic_opt<RA: ResourceAlgebra>(
    a: RA,
    bs: Set<RA>,
)

Expand description

requires

frame_preserving_update_nondeterministic_opt::<RA>(a, bs),

ensures

frame_preserving_update_nondeterministic::<Option<RA>>(Some(a), bs.map(|b| Some(b))),

lemma_frame_preserving_update_nondeterministic_opt