pub proof fn lemma_wf_subset(s: Set<Mapping>, sub: Set<Mapping>)Expand description
requires
wf_mapping_set(s),sub.subset_of(s),sub.finite(),wf_mapping_set(sub),A subset of a wf_mapping_set is also wf.