fact: Definition normImpl (p q : rExpr) := match p, q with | rN p1, rN q1 => rN (rNode rAnd (rN p1) q1) | rN p1, q1 => rN (rNode rAnd (rN p1) (rN q1)) | p1, rN q1 => rN (rNode rAnd p1 q1) | p1, q1 => rN (rNode rAnd p1 (rN q1)) end.