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).
Apply unknownprop_795e291855a044d4d636c961caa1600704603cc02e33a7b37aa66e8d7f6512db 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 4 subgoals.
Let x3 of type ι be given.
Assume H1: x0 x3.
The subproof is completed by applying TrueI.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H1: x0 x3.
Let x4 of type ι → ι → ο be given.
Assume H2:
x4 ((λ x5 x6 x7 . x7) x3 x3 ((λ x5 . lam_id (x1 x5)) x3)) ((λ x5 . lam_id x5) (x1 x3)).
The subproof is completed by applying H2.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H1: x0 x3.
Assume H2: x0 x4.
Assume H3: x0 x5.
Assume H4: x2 x3 x4 x6.
Assume H5: x2 x4 x5 x7.
Let x8 of type ι → ι → ο be given.
Assume H6:
x8 ((λ x9 x10 x11 . x11) x3 x5 ((λ x9 x10 x11 x12 x13 . lam_comp (x1 x9) x12 x13) x3 x4 x5 x7 x6)) ((λ x9 x10 x11 x12 x13 . lam_comp x9 x12 x13) (x1 x3) (x1 x4) (x1 x5) ((λ x9 x10 x11 . x11) x4 x5 x7) ((λ x9 x10 x11 . x11) x3 x4 x6)).
The subproof is completed by applying H6.