+
+definition nat_return := λn:nat. Some ? n.
+
+coercion cic:/matita/test/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/test/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/test/russell/eject_opt.con.
+
+definition find :
+ ∀p:nat → bool.
+ ∀l:list nat. sigma ? (λ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 ]).
+letin program ≝
+ (λp.
+ let rec aux l ≝
+ match l with
+ [ nil ⇒ raise_exn
+ | cons x l ⇒ match p x with [ true ⇒ nat_return x | false ⇒ aux l ]
+ ]
+ in
+ aux);
+apply
+ (program : ∀p:nat → bool.
+ ∀l:list nat. ∃res:option nat.
+ match res with
+ [ None ⇒ ∀y:nat. (mem nat eqb y l = true : Prop) → p y = false
+ | Some (x:nat) ⇒ mem nat eqb x l = true ∧ p x = true ]);
+clear program;
+ [ cases (aux l1); clear aux;
+ simplify in ⊢ (match % in option return ? with [None⇒?|Some⇒?]);
+ generalize in match H2; clear H2;
+ cases a;
+ [ simplify;
+ intros 2;
+ apply (eqb_elim y n);
+ [ intros;
+ autobatch
+ | intros;
+ apply H2;
+ simplify in H4;
+ exact H4
+ ]
+ | simplify;
+ intros;
+ cases H2; clear H2;
+ split;
+ [ elim (eqb n1 n);
+ simplify;
+ autobatch
+ | assumption
+ ]
+ ]
+ | unfold nat_return; simplify;
+ split;
+ [ rewrite > eqb_n_n;
+ reflexivity
+ | assumption
+ ]
+ | unfold raise_exn; simplify;
+ intros;
+ change in H1 with (false = true);
+ destruct H1
+ ]
+qed.
\ No newline at end of file