`{Trichotomy V Vlt} (a b : Quoting.Expr V) vs : toPol a =? toPol b = true -> Quoting.eval _ vs a = Quoting.eval _ vs b. Proof. intros. apply normalize_prequoted. apply eval_eqb;trivial. Qed.
Require Import Import Quoting.Instances.