proposition: Lemma eqb_eq : forall (k1 k2:t) r, (k1 = k2 -> r = true) -> (k1 <> k2 -> r = false) -> (eqb k1 k2) = r.
proof: Proof. intros. destruct (eqb k1 k2) eqn:EQ. - symmetry; apply H. rewrite eqb_spec in EQ; auto. - rewrite eqb_false in EQ. apply H0 in EQ; congruence. Qed.
imports: Lia Cdcl.Coqlib