proposition: Lemma AlphaEqNilAbsP : forall (gs : GSym G) (tma tmb : Pattern gs) (lv : list (vType vc)), pAlphaEq vc tma tmb -> AlphaEqAbs (patAbs vc lv tma) (patAbs vc lv tmb).
proof: Proof. introv Ha. pose proof (GFreshDistRenWSpec vc lv (pAllVars tma++pAllVars tmb++lv)) as XX. exrepnd. repeat (disjoint_reasoning). eapply alAbP with (lbnew := lvn); eauto; unfold pFresh; dands;allsimpl; repeat(disjoint_reasoning); auto;[]. apply alphaEquiVariant; cpx. Qed.
imports: AlphaEquality SwapProps