proposition: Lemma elt_eqb_is_dec : forall k1 k2, elt_eqb k1 k2 = proj_sumbool (elt_eq k1 k2).
proof: Proof. intros. destruct (elt_eq k1 k2); simpl. rewrite K.eqb_spec; auto. rewrite Key.eqb_false. auto. Qed.
imports: Lia Cdcl.Coqlib