blob: 2d5a51345ba76602afdc654a2f42de5262ee4bca (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* Testing eta-expansion of elimination predicate *)
Section NATIND2.
Variable P : nat -> Type.
Variable H0 : (P O).
Variable H1 : (P (S O)).
Variable H2 : (n:nat)(P n)->(P (S (S n))).
Fixpoint nat_ind2 [n:nat] : (P n) :=
<P>Cases n of
O => H0
| (S O) => H1
| (S (S n)) => (H2 n (nat_ind2 n))
end.
End NATIND2.
|
