proposition: Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
proof: Proof. unfold eqke, ltk; intuition; simpl in *; subst. apply lt_not_eq in H. auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance