proposition: Lemma SSubstFilter : disjoint l (fv a) -> tSSubst a s == tSSubst a (filter s l).
proof: Proof. introv Hdis. unfold tSSubst. pose proof ((tcase (@RenAlphaAlpha G vc)) gs a (rangeFreeVars s)) as Hala. pose proof ((tcase (@RenAlphaAlpha G vc)) gs a ((rangeFreeVars (SubFilter s l)))) as Halb. assert ((tRenAlpha a (rangeFreeVars (SubFilter s l))) == (tRenAlpha a (rangeFreeVars s))) as Halc by eauto with Alpha. pose proof (tcase (@RenAlphaAvoid G vc)) as Hav. pose proof (Hav _ a (rangeFreeVars s)) as Havs. apply (ALtcase (@SubstAuxRespectsAlpha G vc)) with (sub:=(SubFilter s l)) in Halc; eauto;[ | repeat (disjoint_reasoning); unfold SubFilter; SetReasoning; fail]. apply (tcase alphaEqSym) in Halc. eapply (tcase alphaEqTransitive); [ | apply Halc]. apply talphaEqRefl. apply (tcase (SSubstAuxSubFilter G vc)). apply alpha_preserves_free_vars in Hala. rw <- Hala. disjoint_reasoning. Qed.
imports: SubstAuxAlphaEq AlphaRen Term