proposition: Lemma pAlphaSwapEmSwap : forall {G : CFGV} {vc : VarSym G}, ( (forall (s : GSym G) (ta : Term s), True) * (forall (s : GSym G) (pta : Pattern s) (sw : Swapping vc), pAlphaEq vc (pSwapEmbed pta sw) (pSwap pta sw)) * (forall (mp : MixtureParam) (ma: Mixture mp) (llbv : list (list (vType vc))) (sw : Swapping vc), (forall b s, LIn (b,s) mp -> b= true) -> lAlphaEqAbs (MakeAbstractions vc (mSwapEmbed ma sw) llbv) (MakeAbstractions vc (mSwap ma sw) 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. - Case "mtcons". introns Hyp. pose proof (Hyp1 _ _ (inl eq_refl)). cpx. Qed.
imports: AlphaEquality SwapProps Eqdep_dec