proposition: Theorem appendIncl2 : forall L1 L2 L3 : list A, append L1 L2 L3 -> InclEq L2 L3.
proof: Proof. intros L1 L2 L3 H'; elim H'; auto with datatypes core. intros a b L4 L5 L6 H'0 H'1 H'2; apply InclEqDef. intros a0 H'3; inversion_clear H'2; inversion_clear H'3; auto. apply InEqComp with (a := b); auto. intros a b L4 L5 L6 H'0 H'1 H'2; apply InclEqDef; auto. intros a0 H'3; inversion_clear H'2; inversion_clear H'3; auto. intros a b L4 L5 L6 H'0 H'1 H'2; apply InclEqDef; auto. intros a0 H'3; inversion_clear H'2; inversion_clear H'3; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)