proposition: Lemma Normal_Equal_eq A (m m' : t A) : Normal m -> Normal m' -> Equal m m' -> m = m'.
proof: Proof. revert m'. induction m as [|l IHl o r IHr]; destruct m' as [|l' o' r']; cbn - [is_empty]; auto. - intros _ (Nl' & Nr' & EY) E. rewrite <- not_true_iff_false in EY. destruct EY. apply is_empty_spec. intros k. now rewrite <- (E k), gleaf. - intros (Nl & Nr & EY) _ E. rewrite <- not_true_iff_false in EY. destruct EY. apply is_empty_spec. intros k. now rewrite (E k), gleaf. - intros (Nl & Nr & EY) (Nl' & Nr' & EY') E. rewrite Equal_node_iff in E. f_equal; intuition. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)