diff options
| -rw-r--r-- | test-suite/success/Inversion.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v new file mode 100644 index 0000000000..96ac86830b --- /dev/null +++ b/test-suite/success/Inversion.v @@ -0,0 +1,15 @@ +(* 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. |