proposition: Lemma alphaEqTransitive : ( (forall (s : GSym G) , transRel (@tAlphaEq _ vc s)) * (forall (s : GSym G), transRel (@pAlphaEq _ vc s)) * transRel (@AlphaEqAbs G vc) * transRel (@lAlphaEqAbs G vc) ).
proof: Proof. intros. GAlphaInd; introns Hyp; intros; allsimpl; trivial; try (econstructor; eauto; fail); [ | | | | | |]. - Case "tnode". inverts Hyp1. EqDecSndEq. subst. rename mb0 into mc. econstructor; eauto with slow. - Case "pvleaf". inverts Hyp. EqDecSndEq. subst. constructor. - Case "pembed". inverts Hyp1; EqDecSndEq; subst; econstructor; eauto with slow. - Case "pnode". inverts Hyp1. EqDecSndEq. subst. rename mb0 into mc. econstructor; eauto with slow. - Case "termAbs". destruct z as [ss lbvc tmc|];[|inversion Hyp5]. duplicate Hyp5 as Htal. apply AlphaEqAbsTSameParam in Hyp5. symmetry in Hyp5. subst. apply (betterAbsTElim (lbnew ++ lbva++ (tAllVars tma))) in Htal. allsimpl. exrepnd. rename lbnew0 into lbcnew. apply (tcase alphaEquiVariant ) in Htal0. specialize (Htal0 (combine lbcnew lbnew)). rewrite (tcase swap_app) in Htal0. rewrite (tcase swap_app) in Htal0. unfold tFresh in Htal3. unfold tFresh in Hyp1. allsimpl. repnd. remAlphaRight Htal0 ll. autorewrite with slow in Htal0; try congruence; cpx; repeat (disjoint_reasoning). apply Hyp4 in Htal0. subst. apply (tcase alphaEquiVariant ) in Htal0. specialize (Htal0 (combine lbnew lbcnew)). remAlphaRight Htal0 ll. rewrite (tcase swap_app) in Htal0. autorewrite with slow in Htal0; try congruence; cpx; repeat (disjoint_reasoning). rewrite (tcase swap_app) in Heqll. rw <- app_assoc in Heqll. rewrite <- (tcase swap_app) in Heqll. rewrite <- (tcase swap_app) in Heqll. rewrite (tcase swapSwitch) in Heqll. rewrite <- AssociationList.ALSwitchCombine in Heqll. rewrite (tcase swapRevNoRep) in Heqll; auto; autorewrite with fast; cpx;[| disjoint_reasoning; fail]. rewrite (tcase swap_app) in Heqll. rewrite (tcase swap_prop_s2Stronger) in Heqll. subst. apply alAbT with (lbnew:=lbcnew); try congruence; [unfolds_base; simpl; dands |]; cpx; repeat (disjoint_reasoning). - Case "patAbs". destruct z as [|ss lbvc tmc];[inversion Hyp5|];[]. duplicate Hyp5 as Htal. apply AlphaEqAbsPSameParam in Hyp5. symmetry in Hyp5. subst. apply (betterAbsPElim (lbnew ++ lbva++ (pAllVars tma))) in Htal. allsimpl. exrepnd. rename lbnew0 into lbcnew. apply (tcase alphaEquiVariant ) in Htal0. specialize (Htal0 (combine lbcnew lbnew)). rewrite (pcase swap_app) in Htal0. rewrite (pcase swap_app) in Htal0. unfold pFresh in Htal3. unfold pFresh in Hyp1. allsimpl. repnd. remAlphaRight Htal0 ll. autorewrite with slow in Htal0; try congruence; cpx; repeat (disjoint_reasoning). apply Hyp4 in Htal0. subst. apply (tcase alphaEquiVariant ) in Htal0. specialize (Htal0 (combine lbnew lbcnew)). remAlphaRight Htal0 ll. rewrite (pcase swap_app) in Htal0. autorewrite with slow in Htal0; try congruence; cpx; repeat (disjoint_reasoning). rewrite (pcase swap_app) in Heqll. rw <- app_assoc in Heqll. rewrite <- (pcase swap_app) in Heqll. rewrite <- (pcase swap_app) in Heqll. rewrite (pcase swapSwitch) in Heqll. rewrite <- AssociationList.ALSwitchCombine in Heqll. rewrite (pcase swapRevNoRep) in Heqll; auto; autorewrite with fast; cpx;[| disjoint_reasoning; fail]. rewrite (pcase swap_app) in Heqll. rewrite (pcase swap_prop_s2Stronger) in Heqll. subst. apply alAbP with (lbnew:=lbcnew); try congruence; [unfolds_base; simpl; dands |]; cpx; repeat (disjoint_reasoning). - Case "laCons". inverts Hyp3. subst. constructor; auto. Qed.
imports: AlphaEquality SwapProps Eqdep_dec