blob: 48e5568e9b927122538b76499828dd98a5edd886 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Set Universe Polymorphism.
Inductive D : nat -> Type :=
| DO : D O
| DS n : D n -> D (S n).
Fixpoint follow (n : nat) : D n -> Prop :=
match n with
| O => fun d => let 'DO := d in True
| S n' => fun d => (let 'DS _ d' := d in fun f => f d') (follow n')
end.
Definition step (n : nat) (d : D n) (H : follow n d) :
follow (S n) (DS n d)
:= H.
|
