proposition: Lemma subtractv_subset : forall sub l, subset (subtractv (rangeFreeVars sub) l) (rangeFreeVars sub).
proof: Proof. unfold subtractv; introv. apply subset_diff. apply subset_app_r; auto. Qed.
imports: Term AssociationList