proposition: Lemma normalize_prequoted `{Trichotomy V Vlt} (a b : Quoting.Expr V) vs : eval phi vs (toPol a) = eval phi vs (toPol b) -> Quoting.eval _ vs a = Quoting.eval _ vs b.
proof: Proof. rewrite !(eval_toPol _). trivial. 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