proposition: Lemma eqb_eq {A} `{E:Eq A} (a b : A) : eqb a b = true <-> a = b.
proof: Proof. destruct (eqb_spec a b); intuition. discriminate. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect