Let x0 of type ι → ο be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι → ι → ο be given.
Assume H0:
∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x2 x3 x4 x5 ⟶ x5 ∈ setexp (x1 x4) (x1 x3).
Assume H1:
∀ x3 . x0 x3 ⟶ x2 x3 x3 (lam_id (x1 x3)).
Assume H2:
∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 x4 x6 ⟶ x2 x4 x5 x7 ⟶ x2 x3 x5 (lam_comp (x1 x3) x7 x6).
Apply unknownprop_3d05796578cdc17ebd2096167db48ecef934256d250d1637eb5dd67225cdfe05 with
x0,
x2,
λ x3 . lam_id (x1 x3),
λ x3 x4 x5 x6 x7 . lam_comp (x1 x3) x6 x7,
λ x3 . True,
HomSet,
λ x3 . lam_id x3,
λ x3 x4 x5 x6 x7 . lam_comp x3 x6 x7,
x1,
λ x3 x4 x5 . x5 leaving 3 subgoals.
Apply unknownprop_1db1571afe8c01990252b7801041a0001ba1fedff9d78947d027d61a0ff0ae7f with
x0,
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_dcf5739aa5fe0adc626fd983737b233fe68652dff14c53b3d75823dcf2542d41.
Apply unknownprop_cb7abf829499aec888363ff9292dd7680786c42dc92f10fdd88dc16ada048723 with
x0,
x1,
x2.
The subproof is completed by applying H0.