proposition: Lemma eq_unique : forall (n m : nat) (h1 h2 : n = m), h1 = h2.
proof: Proof. intros. apply UIP. apply eq_nat_dec. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)