proposition: Lemma RenAlphaNoChange : forall {G : CFGV} {vc : VarSym G}, ( (forall (s : GSym G) (ta : Term s) (lvA : list (vType vc)), disjoint (tBndngVarsDeep vc ta) lvA -> ta = (tRenAlpha ta lvA)) * (forall (s : GSym G) (pta : Pattern s) (lvA : list (vType vc)), disjoint (pBndngVarsDeep vc pta) lvA -> pta = (pRenAlpha pta lvA)) * (forall (l : MixtureParam) (ma: Mixture l) (lvA : list (vType vc)), disjoint (mBndngVarsDeep vc ma) lvA -> ma = mRenAlpha ma lvA)).
proof: Proof. intros. GInduction; introns Hyp; allsimpl; try (f_equal; cpx; fail);[ | | ]. - Case "tnode". f_equal. unfolds_base. cases_ifd Hdd; cpx. rewrite <- mBndngVarsShallowSame in Hddf. provefalse. apply Hddf. SetReasoning. - Case "mtcons". allsimpl. repeat (disjoint_reasoning). f_equal; cpx. - Case "mpcons". allsimpl. repeat (disjoint_reasoning). f_equal; cpx. Qed.
imports: AlphaEqProps Omega