proposition: Lemma AlphaEqNilAbsT : forall (gs : GSym G) (tma tmb : Term gs) (lv : list (vType vc)), tAlphaEq vc tma tmb -> AlphaEqAbs (termAbs vc lv tma) (termAbs vc lv tmb).
proof: Proof. introv Ha. pose proof (GFreshDistRenWSpec vc lv (tAllVars tma++tAllVars tmb++lv)) as XX. exrepnd. repeat (disjoint_reasoning). eapply alAbT with (lbnew := lvn); eauto; unfold tFresh; dands;allsimpl; repeat(disjoint_reasoning); auto;[]. apply alphaEquiVariant; cpx. Qed.
imports: AlphaEquality SwapProps