Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_3189570886a432a72e87efcbd0ea995fafcd88c6ec3c7fdffceb2e344a826cdc with
x2,
λ x3 x4 . In x2 (lam x0 (λ x5 . x1 x5)) ⟶ In (ap x2 1) (x1 x3).
Apply unknownprop_3030666c70e3b0a40e79c3dea18074452b4f067cae53efb13b5a85e3938a9613 with
x2,
λ x3 x4 . In x2 (lam x0 (λ x5 . x1 x5)) ⟶ In x3 (x1 (proj0 x2)).
The subproof is completed by applying unknownprop_90e3c298643df766b84b5eceef5956e9876cb7ac85576c91e0f6a929f73153ed with x0, λ x3 . x1 x3, x2.