proposition: Lemma alphaEqSym : ( (forall (s : GSym G) (ta tb : Term s), tAlphaEq vc ta tb -> tAlphaEq vc tb ta) * (forall (s : GSym G) (pta ptb : Pattern s), pAlphaEq vc pta ptb -> pAlphaEq vc ptb pta) * (forall (aa ab : Abstraction G vc), AlphaEqAbs aa ab -> AlphaEqAbs ab aa) * (forall (la lb : list (Abstraction G vc)), lAlphaEqAbs la lb -> lAlphaEqAbs lb la)).
proof: Proof. intros. GAlphaInd; introns Hyp; intros; try (econstructor; eauto; fail);[|]. - Case "termAbs". eapply alAbT with (lbnew := lbnew); eauto; [eauto with SetReasoning | repeat(disjoint_reasoning)]. - Case "patAbs". eapply alAbP with (lbnew := lbnew); eauto; [eauto with SetReasoning | repeat(disjoint_reasoning)]. Qed.
imports: AlphaEquality SwapProps Eqdep_dec