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