proposition: Lemma betterAbsPElim : forall (gs : GSym G) (lbva lbvb lvAvoid: list vcType) (tma tmb : Pattern gs), AlphaEqAbs (patAbs vc lbva tma) (patAbs vc lbvb tmb) ->{lbnew : list vcType $ let swapa := combine lbva lbnew in let swapb := combine lbvb lbnew in length lbva = length lbnew # length lbvb = length lbnew # pFresh lbnew [tma, tmb] # disjoint (lvAvoid++lbva++lbvb) lbnew # pAlphaEq vc (pSwap tma swapa) (pSwap tmb swapb)}.
proof: Proof. introv Hab. inversion Hab. clear Hab. EqDecSndEq. subst. subst swapa. subst swapb. pose proof (GFreshDistRenWSpec vc lbnew (pAllVars tma++pAllVars tmb++ lbnew ++lbva ++ lbvb++ lvAvoid)) as Hfr. exrepnd. exists lvn. simpl. dands; try congruence; unfold pFresh; allsimpl; dands; repeat(disjoint_reasoning);[]. rename X0 into Htal. apply (tcase alphaEquiVariant ) in Htal. specialize (Htal (combine lbnew lvn)). rewrite (pcase swap_app) in Htal. rewrite (pcase swap_app) in Htal. unfold pFresh in X. allsimpl. repnd. autorewrite with slow in Htal; try congruence; cpx; repeat (disjoint_reasoning). Qed.
imports: AlphaEquality SwapProps Eqdep_dec