proposition: Lemma equal_by_normal `{v: Vars V} `{v': Vars V'} (l r: M) `{!Quote novars l v} `{!Quote v r v'}: ` (monoid_normalization.simplify _ (ua.map_var msig (obvious: False + V → V + V') quote)) ≡ ` (monoid_normalization.simplify _ quote) → l = r.
proof: Proof. Proof with intuition. do 2 destruct monoid_normalization.simplify. simpl. intros. subst. apply (quote_equality l r) . rewrite <- e, <- e0... Qed.
imports: MathClasses.interfaces.abstract_algebra