definition incl : \forall A.(list A) \to (list A) \to Prop \def
\lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
+notation "hvbox(a break ∉ b)" non associative with precedence 45
+for @{ 'notmem $a $b }.
+
+interpretation "list member" 'mem x l = (in_list ? x l).
+interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
+interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
+
lemma not_in_list_nil : \forall A,x.\lnot in_list A x [].
intros.unfold.intro.inversion H
[intros;lapply (sym_eq ? ? ? H2);destruct Hletin
lemma incl_A_A: ∀T,A.incl T A A.
intros.unfold incl.intros.assumption.
-qed.
\ No newline at end of file
+qed.
+
+lemma incl_append_l : ∀T,A,B.incl T A (A @ B).
+unfold incl; intros;autobatch.
+qed.
+
+lemma incl_append_r : ∀T,A,B.incl T B (A @ B).
+unfold incl; intros;autobatch.
+qed.
+
+lemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
+unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
+qed.
+