proposition: Theorem InEqComp : forall (a b : A) (L : list A), InEq a L -> eqA a b -> InEq b L.
proof: Proof. intros a b L H'; generalize b; clear b; elim H'; auto. intros a0 b L0 H'0 b0 H'1. apply InEqHead; auto. apply eqATrans with (y := a0); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)