proposition: Lemma pRenBindersAlpha : forall {G : CFGV} {vc : VarSym G}, ( (forall (s : GSym G) (ta : Term s), True) * (forall (s : GSym G) (pta : Pattern s) (lvA : list (vType vc)), pAlphaEq vc pta (pRenBinders lvA pta)) * (forall (mp : MixtureParam) (ma: Mixture mp) (llbv : list (list (vType vc))) (lvA : list (vType vc)), (forall b s, LIn (b,s) mp -> b= true) -> let maR := mRenBinders lvA ma in lAlphaEqAbs (MakeAbstractions vc ma llbv) (MakeAbstractions vc maR llbv))).
proof: Proof. intros. GInduction; cpx; allsimpl; try (econstructor; eauto with Alpha; fail). - Case "pnode". introns Hyp. allsimpl. constructor. unfold MakeAbstractionsPNode. apply Hyp. introv Hin. apply in_map_iff in Hin; exrepnd; cpx. Qed.
imports: AlphaEqProps Omega