proposition: Theorem InclEqCons : forall (a : A) (L1 L2 : list A), InEq a L2 -> InclEq L1 L2 -> InclEq (a :: L1) L2.
proof: Proof. intros a L1 L2 H' H'0; inversion H'0; auto. apply InclEqDef; auto. intros a0 H'1; inversion H'1; auto. apply InEqComp with (a := a); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)