Let x0 of type ι → ο be given.
Assume H1: ∀ x1 . x0 x1 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x0 x2.
Assume H2:
∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setsum x1 x2).
Apply unknownprop_70eb6d5c4e81105a9bb6d85a6ba8b693c19edf8ca2663bb07fea19af949fed82 with
x0,
HomSet,
λ x1 . lam_id x1,
λ x1 x2 x3 x4 x5 . lam_comp x1 x4 x5 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_fbab5c5311ed298e907b93e9630cf1fbe57c4af2835203632281bf4158a62546 with
x0.
The subproof is completed by applying H1.
Apply unknownprop_7e80016cd90eba8cfb22e412d51217cbc5f2eeece9405f5140e2181ec01c4b9a with
x0.
The subproof is completed by applying H2.