(* Minimisation principle *)

Section Minimal.
Variable P : nat -> Prop.

Inductive Event (n : nat) : Prop :=
   Now : P n -> Event n
 | Fut : Event (S n) -> Event n.

Lemma Event_next n : ~ P n -> Event n -> Event (S n).
intros notP e.
case e; intros.
case notP; trivial.
trivial.
Defined.
Print Event_next.

Variable Pdec : forall n, {P n} + {~ P n}.

Fixpoint findP (n:nat) (e:Event n) : nat := 
     match Pdec n with 
         left _       => n
       | right notPn  => findP (S n) (Event_next n notPn e)
     end.

End Minimal.
Extraction findP.