blob: 44e53ca46caef00d7547e0cc8915db56d4b0723b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
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.
|
