blob: c28e04eb715c015b9f575a1c3d4624ced8f65b3c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(* Submitted by Dachuan Yu (bug #220) *)
Fixpoint T[n:nat] : Type :=
Cases n of
| O => (nat -> Prop)
| (S n') => (T n')
end.
Inductive R : (n:nat)(T n) -> nat -> Prop :=
| RO : (Psi:(T O); l:nat)
(Psi l) -> (R O Psi l)
| RS : (n:nat; Psi:(T (S n)); l:nat)
(R n Psi l) -> (R (S n) Psi l).
Definition Psi00 : (nat -> Prop) := [n:nat] False.
Definition Psi0 : (T O) := Psi00.
Lemma Inversion_RO : (l:nat)(R O Psi0 l) -> (Psi00 l).
Inversion 1.
Abort.
|
