proposition: Theorem OlistUniqueEq : forall (L : list A) (a b : A), Olist (a :: L) -> eqA a b -> ~ InEq b L.
proof: Proof. intros L a b H' H'0; red in |- *; intros H'1; absurd (eqA a b); auto. apply ltAImpNotEqA; auto. apply OlistSupEq with (L := L); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)