Let x0 of type ι → ι be given.
Let x1 of type ι → ι be given.
Claim L1:
(λ x2 . x2) = λ x2 . prim0 (x0 x2) (x1 x2)Apply unknownprop_acde72e2f50237aebb3f280c9adbd840002728dc66b42dda2437acbece7fe515 with
λ x2 . x2,
λ x2 . prim0 (x0 x2) (x1 x2).
The subproof is completed by applying H0.
Apply unknownprop_ebc21f8cd65d757359d6a863b7db31d49a5e6720ea3dbcfcae6a70fd683799e3 with
x0 236c6..,
x1 236c6...
Apply L1 with
λ x2 x3 : ι → ι . (λ x4 . x4) 236c6.. = x2 236c6...
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H2.