proposition: Lemma interpR_wd : forall (e:expr) (x y:R), interpR e x -> (x[=]y) -> interpR e y.
proof: Proof. intros e x y H H0. inversion H; try (rewrite <- H2; rewrite H3 in H1). apply interpR_var. Step_final x. apply interpR_int. Step_final x. apply interpR_plus with x0 y0; auto. Step_final x. apply interpR_mult with x0 y0; auto. Step_final x. apply interpR_unop with x0; auto. Step_final x. apply interpR_binop with x0 y0; auto. Step_final x. apply interpR_part with x0 Hx; auto. Step_final x. Qed.
imports: CoRN.algebra.CRings CoRN.tactics.AlgReflection