`{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. rewrite !(eval_toPol _). trivial. Qed.
Require Import Import Quoting.Instances.