proposition: Lemma alphaEqAlphaSubst : ( (forall (s : GSym G) (t : Term s) (subl subr : SSubstitution vc), AlphaEqSubst subl subr -> tAlphaEq vc (tSSubstAux t subl) (tSSubstAux t subr)) * (forall (s : GSym G) (pt : Pattern s) (subl subr : SSubstitution vc), AlphaEqSubst subl subr -> pAlphaEq vc (pSSubstAux pt subl) (pSSubstAux pt subr)) * (forall (l : MixtureParam) (m : Mixture l) (lbv : list (list (vType vc))) (subl subr : SSubstitution vc), AlphaEqSubst subl subr -> lAlphaEqAbs (MakeAbstractions vc (mSSubstAux m lbv subl) lbv) (MakeAbstractions vc (mSSubstAux m lbv subr) lbv) ) ).
proof: Proof. GInduction; introns Hyp; intros; cpx; allsimpl; try dlist_len lbv; try (econstructor; eauto with slow; fail). - Case "vleaf". ddeq; sp;[| eauto with Alpha; fail]. destruct e. simpl. unfold ALFindDef. dalfind. + eapply ALRangeRelFind in h; eauto. exrepnd. rw h2. sp. + repnud Hyp. apply ALRangeRelSameDom in Hyp. rewrite Hyp in h0. dalfind; cpx;[| eauto with Alpha; fail]. apply ALInEta in h2. dands; cpx. - Case "tnode". constructor. allunfold mAlphaEq. unfold MakeAbstractionsTNode. unfold MakeAbstractionsTNodeAux. unfold allBndngVars. rewrite <- lBoundVarsSameSSubstAux. rewrite <- lBoundVarsSameSSubstAux. cpx. - Case "mtcons". destruct lbv; cpx. + allsimpl. constructor; cpx. eauto with Alpha. + allsimpl. constructor; cpx. apply AlphaEqNilAbsT. apply Hyp. apply ALRangeRelFilter. trivial. - Case "mpcons". destruct lbv; cpx. + allsimpl. constructor; cpx. eauto with Alpha. + allsimpl. constructor; cpx. apply AlphaEqNilAbsP. apply Hyp. apply ALRangeRelFilter. trivial. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux