pub proof fn lemma_set_op_opt<RA: ResourceAlgebra>(s: Set<RA>, t: RA)Expand description
ensures
set_op(s, t).map(|b| Some(b)) == set_op(s.map(|x| Some(x)), Some(t)),pub proof fn lemma_set_op_opt<RA: ResourceAlgebra>(s: Set<RA>, t: RA)set_op(s, t).map(|b| Some(b)) == set_op(s.map(|x| Some(x)), Some(t)),