fact: Definition diffPVarClasses{G} {sa : GSym G} (ta: Pattern sa) {sb: GSym G} (tb : Pattern sb) := match (ta, tb) with | (pvleaf vca va, pvleaf vcb vb) => match (DeqVarSym vca vcb) with |left _ => False |right _ => True end | _ => False end.
imports: AlphaEqProps Omega