+apply rule (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
+[ autobatch;
+| cases s in H; simplify; intros; cases (H H1); ]
+qed.
+
+definition nat_return := λn:nat. Some ? n.
+
+coercion cic:/matita/tests/coercions_russell/nat_return.con.
+
+definition raise_exn := None nat.
+
+definition try_with :=
+ λx,e. match x with [ None => e | Some (x : nat) => x].
+
+lemma hd : list nat → option nat :=
+ λl.match l with [ nil ⇒ raise_exn | cons x _ ⇒ nat_return x ].
+
+axiom f : nat -> nat.
+
+definition bind ≝ λf:nat->nat.λx.
+ match x with [None ⇒ raise_exn| Some x ⇒ nat_return(f x)].
+
+include "datatypes/bool.ma".
+include "list/sort.ma".
+include "nat/compare.ma".
+
+definition inject_opt ≝ λP.λa:option nat.λp:P a. sig_intro ? P ? p.
+
+coercion cic:/matita/tests/coercions_russell/inject_opt.con 0 1.
+
+definition eject_opt ≝ λP.λc: ∃n:option nat.P n. match c with [ sig_intro w _ ⇒ w].
+
+coercion cic:/matita/tests/coercions_russell/eject_opt.con.
+
+(* we may define mem as in the following lemma and get rid of it *)
+definition find_spec ≝
+ λl,p.λres:option nat.
+ match res with
+ [ None ⇒ ∀y. mem ? eqb y l = true → p y = false
+ | Some x ⇒ mem ? eqb x l = true ∧
+ p x = true ∧
+ ∀y.mem ? eqb y l = true → p y = true → x ≠ y →
+ ∃l1,l2,l3.l = l1 @ [x] @ l2 @ [y] @ l3].
+
+lemma mem_x_to_ex_l1_l2 : ∀l,x.mem ? eqb x l = true → ∃l1,l2.l = l1 @ [x] @ l2.
+intros 2; elim l (H hd tl IH H); [simplify in H; destruct H]
+generalize in match H; clear H;
+simplify; apply (eqb_elim x hd); simplify; intros;
+[1:clear IH; rewrite < H; apply (ex_intro ? ? []);
+|2:lapply(IH H1); clear H1 IH; decompose; rewrite > H2; clear H2]
+simplify; autobatch;