proposition: Lemma interpF_wd : forall (e:expr) (x y:F), interpF e x -> (x[=]y) -> interpF e y.
proof: Proof. intros e x y H H0. inversion H; try (rewrite <- H2; rewrite H3 in H1). apply interpF_var. Step_final x. apply interpF_int. Step_final x. apply interpF_plus with x0 y0; auto. Step_final x. apply interpF_mult with x0 y0; auto. Step_final x. apply interpF_unop with x0; auto. Step_final x. apply interpF_binop with x0 y0; auto. Step_final x. apply interpF_part with x0 Hx; auto. Step_final x. apply interpF_div with x0 y0 nzy; auto. Step_final x. Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection