proposition: Lemma RenAlphaAvoid : forall {G : CFGV} {vc : VarSym G}, ( (forall (s : GSym G) (ta : Term s) (lvA : list (vType vc)), disjoint (tBndngVarsDeep vc (tRenAlpha ta lvA)) lvA) * (forall (s : GSym G) (pta : Pattern s) (lvA : list (vType vc)), disjoint (pAlreadyBndBinders vc (pRenAlpha pta lvA)) lvA) * (forall (l : MixtureParam) (ma: Mixture l) (lvA : list (vType vc)), disjoint (mAlreadyBndBinders vc (mRenAlpha ma lvA)) lvA)).
proof: Proof. intros. GInduction; intros; cpx; try (allsimpl; repeat (disjoint_reasoning); cpx; fail);[]. Case "tnode". allsimpl. unfold nodeRenAlpha. specialize (H lvA). remember (mRenAlpha m lvA) as pts. apply ndRenAlAxSpecDisj; auto. Qed.
imports: SubstAux AlphaEqProps