proposition: Lemma alphaEqRefl : ( (forall (s : GSym G) (t : Term s), tAlphaEq vc t t) * (forall (s : GSym G) (pt : Pattern s), pAlphaEq vc pt pt) * (forall (l : MixtureParam) (m : Mixture l) (lbv : list (list (vType vc))), lAlphaEqAbs (MakeAbstractions vc m lbv) (MakeAbstractions vc m lbv))).
proof: Proof. GInduction; introns Hyp; intros; cpx; allsimpl; try dlist_len lbv; try (econstructor; eauto with slow; fail). - Case "mtcons". econstructor; eauto;[]. remember (lhead lbv) as lbvh. apply AlphaEqNilAbsT;cpx. - Case "mpcons". econstructor; eauto;[]. remember (lhead lbv) as lbvh. apply AlphaEqNilAbsP;cpx. Qed.
imports: AlphaEquality SwapProps