proposition: Lemma betterAbsTElim : forall (gs : GSym G) (lbva lbvb lvAvoid: list vcType) (tma tmb : Term gs), AlphaEqAbs (termAbs vc lbva tma) (termAbs 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 # tFresh lbnew [tma, tmb] # disjoint (lvAvoid++lbva++lbvb) lbnew # tAlphaEq vc (tSwap tma swapa) (tSwap tmb swapb)}.
proof: Proof. introv Hab. inversion Hab. clear Hab. EqDecSndEq. subst. subst swapa. subst swapb. pose proof (GFreshDistRenWSpec vc lbnew (tAllVars tma++tAllVars tmb++ lbnew ++lbva ++ lbvb++ lvAvoid)) as Hfr. exrepnd. exists lvn. simpl. dands; try congruence; unfold tFresh; allsimpl; dands; repeat(disjoint_reasoning);[]. rename X0 into Htal. apply (tcase alphaEquiVariant ) in Htal. specialize (Htal (combine lbnew lvn)). rewrite (tcase swap_app) in Htal. rewrite (tcase swap_app) in Htal. unfold tFresh in X. allsimpl. repnd. autorewrite with slow in Htal; try congruence; cpx; repeat (disjoint_reasoning). Qed.
imports: AlphaEquality SwapProps Eqdep_dec