proposition: Lemma fexprF2interpF : forall e:fexprF, interpF (fforgetF e) (finterpF e).
proof: Proof. intros e. elim e. intros x e'. unfold fforgetF in |- *. simpl in |- *. apply xexprF2interpF. Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection