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