proposition: Lemma alphaEqDecidable : forall {G} (vc : VarSym G), ( (forall (sa : GSym G) (ta: Term sa) (sb: GSym G) (tb : Term sb), decidable (tAlphaEqG vc ta tb)) * (forall (sa : GSym G) (ta: Pattern sa) (sb: GSym G) (tb : Pattern sb), decidable (pAlphaEqG vc ta tb)) * (forall (l : MixtureParam) (ma mb : Mixture l) (lbva : list (list (vType vc))) (lbvb : list (list (vType vc))), decidable (lAlphaEqAbs (MakeAbstractions vc ma lbva) (MakeAbstractions vc mb lbvb)))).
proof: Proof. intros. GInductionS; introns Hyp; intros; allsimpl. - Case "tleaf". destruct tb;[ | right; notAlpha | right; notAlpha];[]. EqDec T T0; [| right; notAlpha]; subst. EqDec t t0; [left|right]; subst; unfold tAlphaEqG; try rewrite DeqTrue; allsimpl; eauto with Alpha;[]; notAlpha. - Case "vleaf". destruct tb; [right; notAlpha | |]. + EqDec vc0 vc1;[| right]; subst; try EqDecRefl; simpl. * EqDec v v0; [left|right]; subst; unfolds_base; try rewrite DeqTrue; eauto with Alpha. notAlpha. * notAlpha. revert Hseqd0. remember (vleaf vc0 v) as vvl. remember (vleaf vc1 v0) as vvr. assert ( diffVarClasses vvl vvr) as Hdd by (subst; unfold diffVarClasses; cases_if; cpx). clear Heqvvr Heqvvl. remember (vSubstType G vc0). remember (vSubstType G vc1). generalize dependent vvl. generalize dependent vvr. rewrite H0. intros. allsimpl. EqDecRefl. simpl. clear dependent t. clear Hneqvc0vc1. clear v0 v vc0 Heqt0 Hseqd0 vc1. introv Hc; inverts Hc; EqDecSndEq; subst vvl; subst vvr; repnud Hdd; allsimpl; cpx. rewrite DeqTrue in Hdd. trivial. + right. notAlpha. introv Hal. inverts Hal. EqDecSndEq. GC. clear H6. clear X. clear H0. generalize dependent H3. remember (vleaf vc0 v) as xx. assert (isVLeaf xx) as Hxx by (subst;simpl; auto). clear Heqxx. generalize dependent xx. rewrite Hseqd0. allsimpl. introv Hisv Heq. inverts keep Heq. cpx. - Case "tnode". destruct tb; [right; notAlpha;fail | |]. right. notAlpha; remember (vleaf vc0 v) as xx. assert (isVLeaf xx) as Hxx by (subst;simpl; auto). clear Heqxx. generalize dependent xx. rewrite <- Hseqd0. allsimpl. introv Hisv Heq. inverts Heq. EqDecSndEq. subst xx. cpx; fail. EqDec p p0;[| right]. Focus 2. notAlpha. introv Hal. remember (tnode p m) as vvl. remember (tnode p0 m0) as vvr. assert (diffTProdsNode vvl vvr) as Hdd by (subst; unfold diffTProdsNode; cases_if; cpx). clear Heqvvr Heqvvl. remember (tpLhs G p). remember (tpLhs G p0). generalize dependent vvl. generalize dependent vvr. generalize Hseqd0. rewrite H0. introv. allsimpl. EqDecRefl. simpl. clear dependent t. introv Hta Hdd. clear Hseqd1 Heqt0 Hneqpp0 m0 Hyp m. inverts Hta; EqDecSndEq; subst vvl; subst vvr; repnud Hdd; allsimpl; cpx. rewrite DeqTrue in Hdd; trivial; fail. subst p0. unfold tAlphaEqG. rewrite DeqTrue. simpl. rename m0 into mb. destruct (Hyp mb (allBndngVars vc p m) (allBndngVars vc p mb)) as [Hleq | Hnleq];[left; constructor;auto | right; notAlpha]. - Case "ptleaf". destruct tb;[ | right; notAlpha | right; notAlpha | right; notAlpha]; []. EqDec T T0; [| right; notAlpha]; subst;[]. EqDec t t0; [left|right]; subst; unfold pAlphaEqG; try rewrite DeqTrue; allsimpl; eauto with Alpha;[]; notAlpha. - Case "pvleaf". destruct tb;[ right; notAlpha | | right; notAlpha | right; notAlpha]; []. EqDec vc0 vc1;[ left;subst; try EqDecRefl; simpl; unfold pAlphaEqG; rewrite DeqTrue ; constructor; fail | right; notAlpha]. - Case "pembed". destruct tb;[ right; notAlpha | right; notAlpha | | right; notAlpha]. Focus 2. introv Hal. inverts Hal. EqDecSndEq. GC. clear H6. clear X. clear H0. generalize dependent H3. remember (embed p t) as xx. assert (isEmbed xx) as Hxx by (subst;simpl; auto). clear Heqxx. generalize dependent xx. rewrite Hseqd0. allsimpl. introv Hisv Heq. inverts keep Heq. cpx; fail. EqDec p p0;[ subst p0; unfold pAlphaEqG; rewrite DeqTrue | right; notAlpha]. Focus 2. remember (embed p t) as vvl. remember (embed p0 t0) as vvr. assert (diffEmbedNode vvl vvr) as Hdd by (subst; unfold diffEmbedNode; cases_if; cpx). clear Heqvvr Heqvvl. remember (epLhs G p). remember (epLhs G p0). generalize dependent vvl. generalize dependent vvr. generalize Hseqd0. rewrite H0. introv. allsimpl. EqDecRefl. simpl. clear dependent p. introv Hta Hdd. clear H0 Hseqd1 Hseqd0 Heqp2 p1 t0 p0. inverts Hdd; EqDecSndEq; subst vvl; subst vvr; repnud Hta; allsimpl; cpx. rewrite DeqTrue in Hta; trivial; fail. simpl. pose proof (Hyp _ t0) as Hd. unfold tAlphaEqG in Hd. rewrite DeqTrue in Hd. simpl in Hd. destruct Hd;[left; constructor; trivial | right; notAlpha]. - Case "pnode". destruct tb;[ right; notAlpha | right; notAlpha | right; notAlpha| ]. introv Hal. inverts Hal. EqDecSndEq. GC. clear H6. clear X. clear H0. generalize dependent H3. remember (pnode p m) as xx. assert (isPNode xx) as Hxx by (subst;simpl; auto). clear Heqxx. generalize dependent xx. rewrite Hseqd0. allsimpl. introv Hisv Heq. inverts keep Heq. cpx; fail. EqDec p p0;[| right]. Focus 2. notAlpha. remember (pnode p m) as vvl. remember (pnode p0 m0) as vvr. assert (diffPProdsNode vvl vvr) as Hdd by (subst; unfold diffPProdsNode; cases_if; cpx). clear Heqvvr Heqvvl. remember (ppLhs G p). remember (ppLhs G p0). generalize dependent vvl. generalize dependent vvr. generalize Hseqd0. rewrite H0. introv. allsimpl. EqDecRefl. simpl. clear dependent p. introv Hta Hdd. clear H0 Hseqd1 Hseqd0 Heqp2 p1 m0 p0. inverts Hdd; EqDecSndEq; subst vvl; subst vvr; repnud Hta; allsimpl; cpx. rewrite DeqTrue in Hta; trivial; fail. subst p0. unfold pAlphaEqG. rewrite DeqTrue. simpl. rename m0 into mb. destruct (Hyp mb [] []) as [Hleq | Hnleq];[left; constructor;auto | right; notAlpha]. - Case "mnil". dependent inversion mb. simpl. left. constructor. - Case "mtcons". dependent inversion mb. simpl. subst. remember (lhead lbva) as lha. remember (lhead lbvb) as lhb. remember (tail lbva) as lta. remember (tail lbvb) as ltb. clear Heqlha Heqlhb Heqlta Heqltb. specialize (Hyp0 m lta ltb). destruct (Hyp0); [| right ; notAlpha]. destruct (decideAbsT vc ph Hyp h t lha lhb); [left; constructor; auto| right; notAlpha]. - Case "mpcons". dependent inversion mb. simpl. subst. remember (lhead lbva) as lha. remember (lhead lbvb) as lhb. remember (tail lbva) as lta. remember (tail lbvb) as ltb. clear Heqlha Heqlhb Heqlta Heqltb. specialize (Hyp0 m lta ltb). destruct (Hyp0); [| right ; notAlpha]. destruct (decideAbsP vc ph Hyp h p lha lhb); [left; constructor; auto| right; notAlpha]. Defined.
imports: AlphaEqProps Omega