Apply unknownprop_74210cc9b2960bdcb3eab56d0b4f5ba5a5771478f68cd794d919dafbcd157b00 with
λ x0 x1 : ι → ι . ∀ x2 x3 . In (x0 x3) x2 ⟶ In x3 (proj0 x2).
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_066957b70daa6a29576d33100fc785e639cd0f9409f03710c5d2ba808ef62ce1 with
λ x2 x3 : ι → ι . In x1 (x3 x0).
Apply unknownprop_05a8fb1492e1d649432d99059efe6cb5519f68cbf274db02d816fcaae9af18ba with
x1,
λ x2 x3 . In x2 (ReplSep x0 (λ x4 . ∃ x5 . Inj0 x5 = x4) (λ x4 . Unj x4)).
Apply unknownprop_8d2d2cad5b49b3f5b663b34a4b05b87bd91c0d0340dcf2eab94b6803f88f2fd8 with
x0,
λ x2 . ∃ x3 . Inj0 x3 = x2,
Unj,
Inj0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ο be given.
Assume H1:
∀ x3 . Inj0 x3 = Inj0 x1 ⟶ x2.
Apply H1 with
x1.
Let x3 of type ι → ι → ο be given.
The subproof is completed by applying H2.