fact: Definition pAlphaEqG {G} (sa sb : GSym G) (vc: VarSym G ) (ta : Pattern sa) (tb : Pattern sb):= match (deqGSym sa sb) with | left eqq => pAlphaEq vc (transport eqq ta) tb | right eqq => False end.
imports: AlphaEqProps Omega