proposition: Lemma SubstFilterDisjAux: forall sub lbva lbcnew, disjoint (lbva ++ lbcnew) (rangeFreeVars sub) -> disjoint lbcnew (ALDom sub) -> disjoint (ALDom (ALFilter (DeqVtype vc) sub lbva) ++ rangeFreeVars (ALFilter (DeqVtype vc) sub lbva)) (lbva ++ lbcnew).
proof: Proof. introv H1d H2d. rewrite <- ALDomFilterCommute. repeat(disjoint_reasoning); cpx. - apply disjoint_diff_l. rewrite diffSameNil. auto. - SetReasoning. - apply disjoint_diff_l. SetReasoning. apply subset_diff. SetReasoning. - clear H2d. SetReasoning. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux