proposition: Theorem inclImpImplEq : forall L1 L2 : list A, incl L1 L2 -> InclEq L1 L2.
proof: Proof. intros L1 L2 H'; apply InclEqDef. intros a H'0; generalize H'; elim H'0; auto. intros a0 b L H'1 H'2. apply InEqComp with (a := b); auto. apply inImpInEq; auto with datatypes core. intros a0 b L H'1 H'2 H'3. apply H'2; auto. apply incl_tran with (A := A) (m := b :: L); auto with datatypes core. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)