-(* intros 4;elim l
- [elim (not_in_list_nil ? ? H)
- |elim (in_list_cons_case ? ? ? ? H1)
- [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
- |simplify;apply (bool_elim ? (p a));intro;simplify;
- [apply in_list_cons;apply H;assumption
- |apply H;assumption]]]
-qed.*)
-
-naxiom incl_A_A: ∀T,A.incl T A A.
-(*intros.unfold incl.intros.assumption.
-qed.*)
-
-naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
-(*unfold incl; intros;autobatch.
-qed.*)
-
-naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
-(*unfold incl; intros;autobatch.
-qed.*)
-
-naxiom 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.*)
+#A al0 p a0;nelim al0
+##[#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/
+##|#a1 al1 IH H1 H2;ncases (in_list_cons_case ???? H1);#H3
+ ##[nnormalize;nrewrite < H3;nrewrite > H2;@
+ ##|nnormalize;ncases (p a1);nnormalize;
+ ##[@2;napply IH;//
+ ##|napply IH;//
+ ##]
+ ##]
+##]
+nqed.
+
+nlemma incl_A_A: ∀T,A.incl T A A.
+#A al0 a0 H1;//;
+nqed.
+
+nlemma incl_append_l : ∀T,A,B.incl T A (A @ B).
+#A al0 al1 a0 H1;/2/;
+nqed.
+
+nlemma incl_append_r : ∀T,A,B.incl T B (A @ B).
+#A al0 al1 a0 H1;/2/;
+nqed.
+
+nlemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
+#A al0 al1 a0 H1 a1 H2;ncases (in_list_cons_case ???? H2);/2/;
+#H3;@2;napply H1;//;
+nqed.