fact: Definition swapEmbedAbs {G : CFGV} {vc : VarSym G} (a : Abstraction G vc) (sw : Swapping vc) : (Abstraction G vc):= match a with | termAbs _ lbv t => termAbs _ lbv t | patAbs _ lbv t => patAbs _ lbv (pSwapEmbed t sw) end.
imports: AlphaEqProps Omega