proposition: Lemma fexprR2interp : forall e:fexprR, interpR (fforgetR e) (finterpR e).
proof: Proof. intros e. elim e. intros x e'. unfold fforgetR in |- *. simpl in |- *. apply xexprR2interpR. Qed.
imports: CoRN.algebra.CRings CoRN.tactics.AlgReflection