proposition: Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''.
proof: Proof. unfold ltk, eqk. destruct e, e', e''. simpl. intros; subst; trivial. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses