proposition: Lemma decideAbsP {G} (vc : VarSym G) (sa : GSym G) (ta: Pattern sa) (Hdt : forall phnew : Pattern sa, pSize phnew <= pSize ta -> forall (sb : GSym G) (tb : Pattern sb), decidable (pAlphaEqG vc phnew tb)) (sb : GSym G) (tb: Pattern sa) (la lb :(list (vType vc))) : decidable (AlphaEqAbs (patAbs vc la ta) (patAbs vc lb tb)).
proof: Proof. remember (beq_nat (length la) (length lb)) as blen. destruct blen; [ applysym beq_nat_true in Heqblen | right ; applysym beq_nat_false in Heqblen; introv Hal; inverts Hal; EqDecSndEq; omega ]. remember (GFreshVars (la++lb ++ pAllVars ta++pAllVars tb) la) as lvn. remember (pSwap ta (combine la lvn)) as phnew. pose proof (pcase (@swapPreservesSize G vc (combine la lvn)) _ ta) as Hs. specialize (Hdt (pSwap ta (combine la lvn))). rewrite Hs in Hdt. dimp Hdt. apply Hdt with (tb:= (pSwap tb (combine lb lvn))) in hyp. unfold pAlphaEqG in hyp. rewrite DeqTrue in hyp. allsimpl. clear Hs Hdt. clear dependent phnew. destruct hyp as [? | Hnal];[left| right]; pose proof (FreshDistVarsSpec (la ++ lb ++ pAllVars ta ++ pAllVars tb) la ) as XX; rewrite <- Heqlvn in XX; simpl in XX; repnd; dands; symmetry in XX. - apply alAbP with (lbnew:=lvn); cpx; try congruence; unfold pFresh; allsimpl; repeat(disjoint_reasoning). - introv Hal. apply Hnal. clear Hnal. clear Heqlvn. apply betterAbsPElim with (lvAvoid:= lvn) in Hal. allsimpl. exrepnd. apply pAlphaEqEquivariantRev with (sw := combine lvn lbnew). autorewrite with SwapAppR. unfold pFresh in Hal3. allsimpl. repnd. symmetry in XX. autorewrite with slow; try congruence; cpx; repeat (disjoint_reasoning); repeat match goal with [ H : disjoint _ _ |- _ ] => clear H | [ H : no_repeats _ _ |- _ ] => clear H end. Defined.
imports: AlphaEqProps Omega