proposition: Lemma Norm_wfF : forall e:expr, wfF F val unop binop pfun e -> wfF F val unop binop pfun (NormF e).
proof: Proof. unfold wfF in |- *. intros. elim X. intros. exists x. apply NormF_corr. assumption. Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection