blob: 63137edbac8ccfc1f97c272f262a7506f7f89873 (
plain)
1
2
3
4
5
6
7
8
9
|
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
|
