fact: Definition diffEmbedNode {G} {sa : GSym G} (ta: Pattern sa) {sb: GSym G} (tb : Pattern sb) := match (ta, tb) with | (embed pa va, embed pb vb) => match (deqEm G pa pb) with |left _ => False |right _ => True end | _ => False end.
imports: AlphaEqProps Omega