proposition: Lemma RenAlphaAlpha : forall {G : CFGV} {vc : VarSym G}, ( (forall (s : GSym G) (ta : Term s) (lvA : list (vType vc)), tAlphaEq vc ta (tRenAlpha ta lvA)) * (forall (s : GSym G) (pta : Pattern s) (lvA : list (vType vc)), pAlphaEq vc pta (pRenAlpha pta lvA)) * (forall (l : MixtureParam) (ma: Mixture l) (llbv : list (list (vType vc))) (lvA : list (vType vc)), let maR := mRenAlpha ma lvA in lAlphaEqAbs (MakeAbstractions vc ma llbv) (MakeAbstractions vc maR llbv))).
proof: Proof. intros. GInduction; intros; cpx; try (econstructor; eauto; fail);[| |]. - Case "tnode". allsimpl. constructor. unfold MakeAbstractionsTNode. unfold nodeRenAlphaAux. eapply (alphaEqTransitive); [ |apply ndRenAlAxAlpha with (lvA0 := lvA); eauto]. unfold MakeAbstractionsTNodeAux. rw <- (@mRenlBinderShallowSame G vc). apply X; cpx. unfold tpRhsAugIsPat. unfold prhsIsBound. rw combine_length. unfold tpRhsSym. autorewrite with fast. rw min_eq; auto. apply bndngPatIndicesValid2; auto. - Case "mtcons". subst maR. allunfold MakeAbstractionsTNodeAux. simpl. constructor; cpx. apply AlphaEqNilAbsT; cpx. - Case "mpcons". subst maR. allunfold MakeAbstractionsTNodeAux. simpl. constructor; cpx. apply AlphaEqNilAbsP; cpx. Qed.
imports: AlphaEqProps Omega