proposition: Lemma refl_interpR : forall (e:expr) (x y:R), interpR e x -> interpR e y -> x[=]y.
proof: Proof. intro e. induction e. intros x y Hx Hy. inversion Hx. inversion Hy. Step_final (val v). intros x y Hx Hy. inversion Hx. inversion Hy. Step_final (zring z:R). intros x y H1 H2. inversion H1. inversion H2. astepl (x0[+]y0). Step_final (x1[+]y1). intros x y H1 H2. inversion H1. inversion H2. astepl (x0[*]y0). Step_final (x1[*]y1). intros x y H0 H1. inversion H0. intros x y H0 H1. inversion H0. inversion H1. astepl (unop u x0); Step_final (unop u x1). intros x y H0 H1. inversion H0. inversion H1. astepl (binop b x0 y0); Step_final (binop b x1 y1). intros x y H0 H1. inversion H0. inversion H1. astepl (pfun p x0 Hx); Step_final (pfun p x1 Hx0). Qed.
imports: CoRN.algebra.CRings CoRN.tactics.AlgReflection