blob: 1facd9b7e90bc3cf35c8a9cb69e51d93f9d0b4fa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Check let TTT := Type in (fun (a b : @sigT TTT (fun A : TTT => A))
(f : @projT1 TTT (fun A : TTT => A) a ->
@projT1 TTT (fun A : TTT => A) b) =>
@eq_refl
(@projT1 TTT (fun A : TTT => A) a ->
@projT1 TTT (fun A : TTT => A) b)
(fun x : @projT1 TTT (fun A : TTT => A) a => f x)) :
forall (a b : @sigT TTT (fun A : TTT => A))
(f : @projT1 TTT (fun A : TTT => A) a ->
@projT1 TTT (fun A : TTT => A) b),
@eq
(@projT1 TTT (fun A : TTT => A) a ->
@projT1 TTT (fun A : TTT => A) b)
(fun x : @projT1 TTT (fun A : TTT => A) a => f x) f.
|
