proposition: Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''.
proof: Proof. unfold eqke; intros [k1 e1] [k2 e2] [k3 e3]; simpl; now intros [-> ->]. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance