fact: Fixpoint norm (e : Expr) : rExpr := match e with | V n => rV n | normalize.N p => normNot (norm p) | Node n1 p q => match n1 with | ANd => rNode rAnd (norm p) (norm q) | Or => normOr (norm p) (norm q) | Impl => normImpl (norm p) (norm q) | normalize.Eq => rNode rEq (norm p) (norm q) end end.