proposition: Lemma SSubstFVarsDisjoint: forall (s : GSym G) (t : Term s) (sub : SSubstitution vc) lf, disjoint (tfreevars vc t) lf -> disjoint (rangeFreeVars sub) lf -> disjoint (tfreevars vc (tSSubst t sub)) lf.
proof: Proof. introv H1d H2d. pose proof (tRenWithSpec t (fvr sub)) as Hfr. exrepnd. duplicate Hfr1 as Hb. apply (ALtcase alpha_preserves_free_vars) in Hb. rewrite Hb in H1d. clear Hb. apply SSubstRespectsAlpha1 with (sa:=sub) in Hfr1. apply (ALtcase alpha_preserves_free_vars) in Hfr1. rewrite Hfr1. rename tar into ar. clear dependent t. unfold tSSubst. rewrite <- (tcase RenAlphaNoChange) by cpx. introv Hin. apply (tcase (@free_vars_SSubstAux G vc)) in Hin; cpx;[]. rw in_app_iff in Hin. dorn Hin; cpx. + apply in_diff in Hin. repnd. introv Hinc; disjoint_lin_contra. + rw disjoint_flat_map_l in H2d. allsimpl. rw lin_flat_map in Hin. exrepnd. rw in_map_iff in Hin1. exrepnd. allsimpl. subst. rw ALKeepFirstLin in Hin1. repnd. apply ALFindSome in Hin2. apply ALInEta in Hin2. repnd. apply H2d in Hin2. apply Hin2. cpx. Qed.
imports: SubstAuxAlphaEq AlphaRen Term