proposition: Lemma alphaEquiVariant : ( (forall (s : GSym G) , EquiVariantRelSame (@tSwap G vc s) (tAlphaEq vc)) * (forall (s : GSym G), EquiVariantRelSame (@pSwap G vc s) (pAlphaEq vc)) * (EquiVariantRelSame (@swapAbs G vc) (@AlphaEqAbs G vc)) * (EquiVariantRelSame (@swapLAbs G vc) (@lAlphaEqAbs G vc)) ).
proof: Proof. intros. GAlphaInd; introns Hyp; intros; allsimpl; try (econstructor; eauto; fail);[| | |]. - Case "tnode". constructor. unfold allBndngVars. rw <- swapLBoundVarsCommute. rw <- swapLBoundVarsCommute. rewrite <- MakeLAbsSwapCommute. rewrite <- MakeLAbsSwapCommute. cpx. - Case "pnode". constructor. rewrite <- MakeAbsPNodeCommute. rewrite <- MakeAbsPNodeCommute. cpx. - Case "termAbs". specialize (Hyp4 sw). rewrite (tcase swap_app) in Hyp4. rewrite (tcase swap_app) in Hyp4. rewrite (tcase swap_prop_e1Stronger) in Hyp4. match type of Hyp4 with tAlphaEq _ _ ?b => pattern b in Hyp4 end. rewrite (tcase swap_prop_e1Stronger) in Hyp4. rewrite <- (tcase swap_app) in Hyp4. rewrite <- (tcase swap_app) in Hyp4. unfold swapSwap in Hyp4. rewrite map_combine in Hyp4. rewrite map_combine in Hyp4. fold (swapLVar sw lbva) in Hyp4. fold (swapLVar sw lbvb) in Hyp4. fold (swapLVar sw lbnew) in Hyp4. remember (swapLVar sw lbnew) as lbns. repnud Hyp1. allsimpl. eapply alAbT with (lbnew := lbns); eauto; try ( subst; unfold swapLVar; autorewrite with fast; congruence; fail); cpx; subst;[unfolds_base; allsimpl; dands|];repeat (disjoint_reasoning);[ | | | | ]. + rewrite <- (tcase AllVarsEquivariant). apply DisjointEquivariant; trivial. + rewrite <- (tcase AllVarsEquivariant). apply DisjointEquivariant; trivial. + apply NoRepeatsEquivariant; trivial. + apply DisjointEquivariant; trivial. + apply DisjointEquivariant; trivial. - Case "patAbs". specialize (Hyp4 sw). rewrite (pcase swap_app) in Hyp4. rewrite (pcase swap_app) in Hyp4. rewrite (pcase swap_prop_e1Stronger) in Hyp4. match type of Hyp4 with pAlphaEq _ _ ?b => pattern b in Hyp4 end. rewrite (pcase swap_prop_e1Stronger) in Hyp4. rewrite <- (pcase swap_app) in Hyp4. rewrite <- (pcase swap_app) in Hyp4. unfold swapSwap in Hyp4. rewrite map_combine in Hyp4. rewrite map_combine in Hyp4. fold (swapLVar sw lbva) in Hyp4. fold (swapLVar sw lbvb) in Hyp4. fold (swapLVar sw lbnew) in Hyp4. remember (swapLVar sw lbnew) as lbns. repnud Hyp1. allsimpl. eapply alAbP with (lbnew := lbns); eauto; try ( subst; unfold swapLVar; autorewrite with fast; congruence; fail); cpx; subst;[unfolds_base; allsimpl; dands|];repeat (disjoint_reasoning);[ | | | | ]. + rewrite <- (pcase AllVarsEquivariant). apply DisjointEquivariant; trivial. + rewrite <- (pcase AllVarsEquivariant). apply DisjointEquivariant; trivial. + apply NoRepeatsEquivariant; trivial. + apply DisjointEquivariant; trivial. + apply DisjointEquivariant; trivial. Qed.
imports: AlphaEquality SwapProps