1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
21 inductive Q : nat -> T -> Prop :=
23 | lr : ∀n,t.Q (S (S n)) t -> Q n (r t).
27 definition xxx := λt.(match t return (λt:T.T) with
28 [ l => match F in False with []
31 let rec f (n:nat) (t:T) on t :nat :=
35 f (S (S mmm)) (xxx t)]).
37 let rec f (n:nat) (t:T) on t : Q n t -> nat :=
40 | S mmm => λq:Q (S mmm) (r t).
42 (match t return (λt:T.T) with
43 [ l => match F in False with []
46 (match q return λn,t,x.Q (S (S n)) t with
47 [ lq => match F in False return λ_.Q (S (S n)) t with []
48 | lr k t qsskt => qsskt])