proposition: Lemma eq_list_refl: forall a, eq_list a a.
proof: Proof. intro a. induction a; intros. - now simpl. - simpl. destruct a as (k, e). case_eq (compare k k); intros. + revert H. generalize l. apply lt_not_eq in l. now contradict l. + split; easy. + revert H. generalize l. apply lt_not_eq in l. now contradict l. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses ProofIrrelevance