proposition: Lemma Tactic_lemma_zero_F : forall (x:F) (e:xexprF F val unop binop pfun x), expr_is_zero (NormF (xforgetF _ _ _ _ _ _ e)) = true -> x[=][0].
proof: Proof. intros. apply refl_interpF with val unop binop pfun (NormF (xforgetF _ _ _ _ _ _ e)). apply NormF_corr. apply xexprF2interpF. apply expr_is_zero_corr_F. apply Norm_wfF. apply xexprF2wfF. assumption. Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection