blob: 3c440b9d028de68a1a4f69f5e0c24d0a9a96a92e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
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 _ 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
proj =
fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
match eq_nat_dec x y with
| left eqprf =>
match eqprf in (_ = z) return (P z) with
| refl_equal => def
end
| right _ => prf
end
: forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
Argument scopes are [nat_scope nat_scope _ _ _]
|
