blob: b63ffd926a07d8a2ee28fa70a278ef1ed405d683 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
t_rect =
fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
fix F (t : t) : P t :=
match t as t0 return (P t0) with
| k x x0 => f x0 (F x0)
end
: forall P : t -> Type,
(let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
= (1, 3)
: (nat * nat)%type
= (1, 2)
: (nat * nat)%type
|
