`{Q : @Quoting.EqQuote R _ _ _ _ _ V l n m V' l'} `{Trichotomy V Vlt} `{Trichotomy V' Vlt'} : toPol (Quoting.expr_map inl (@Quoting.eqquote_l R _ _ _ _ _ _ _ _ _ _ _ Q)) =? toPol (@Quoting.eqquote_r R _ _ _ _ _ _ _ _ _ _ _ Q) = true -> n = m. Proof. intros E. apply normalize_eq. apply eval_eqb,E. Qed.
Require Import Import Quoting.Instances.