proposition: Lemma SubstSubFVarsDisjoint: forall (sa sb : SSubstitution vc) lf, disjoint (fvr sa ++ fvr sb) lf -> disjoint (fvr (SubstSub sa sb)) lf.
proof: Proof. induction sa as [| (v,t) sa Hind]; introv Hd; allsimpl; [unfold rangeFreeVars; cpx |]. rewrite rangeFreeVars_cons. rewrite rangeFreeVars_cons in Hd. repeat (disjoint_reasoning); cpx; [|apply Hind; repeat (disjoint_reasoning)]. apply SSubstFVarsDisjoint; auto. Qed.
imports: SubstAuxAlphaEq AlphaRen Term