proposition: Lemma Tactic_lemmaR : forall (x y:R) (e:xexprR R val unop binop pfun x) (f:xexprR R val unop binop pfun y), eq_expr (NormR (xforgetR _ _ _ _ _ _ e)) (NormR (xforgetR _ _ _ _ _ _ f)) = true -> x[=]y.
proof: Proof. intros x y e f H. apply refl_interpR with val unop binop pfun (NormR (xforgetR _ _ _ _ _ _ e)). apply NormR_corr; apply xexprR2interpR. rewrite (eq_expr_corr _ _ H). apply NormR_corr; apply xexprR2interpR. Qed.
imports: CoRN.algebra.CRings CoRN.tactics.AlgReflection