proposition: Lemma normalize_eq `{Q : @Quoting.EqQuote R _ _ _ _ _ V l n m V' l'} `{Trichotomy V Vlt} `{Trichotomy V' Vlt'} : eval phi (Quoting.merge R l l') (toPol (Quoting.expr_map inl (Quoting.eqquote_l R))) = eval phi (Quoting.merge R l l') (toPol (Quoting.eqquote_r R)) -> n = m.
proof: Proof. intros E. eapply Quoting.eval_eqquote. etransitivity;[symmetry;apply (eval_toPol _)|]. etransitivity;[|apply (eval_toPol _)]. exact E. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.tactics.ring_quote HoTT.Classes.tactics.ring_pol HoTT.Classes.theory.rings HoTT.Classes.orders.sum HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.integers