proposition: Lemma in_ALRange_ALFilter_implies : forall (sub : SSubstitution vc) l, subset (ALRange (SubFilter sub l)) (ALRange sub).
proof: Proof. unfold SubFilter. unfold subset, ALRange; introv i. allrw in_map_iff; exrepnd; allsimpl; subst. exists (a0,a); simpl; sp. allapply ALFilterLIn; sp. Qed.
imports: Term AssociationList