`{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. intros E. eapply Quoting.eval_eqquote. etransitivity;[symmetry;apply (eval_toPol _)|]. etransitivity;[|apply (eval_toPol _)]. exact E. Qed.
Require Import Import Quoting.Instances.