Apply unknownprop_ca4ccf6887ff6dc7b05e5402a8b941f864c9703226396122edada9d3d18a208b with
λ x0 x1 : ι → (ι → ο) → (ι → ι) → ι . ∀ x2 . ∀ x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 . In x5 (x1 x2 (λ x6 . x3 x6) (λ x6 . x4 x6)) ⟶ ∃ x6 . and (and (In x6 x2) (x3 x6)) (x5 = x4 x6).
Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι → ι be given.
Let x3 of type ι be given.
Assume H0:
In x3 (Repl (Sep x0 (λ x4 . x1 x4)) (λ x4 . x2 x4)).
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with
Sep x0 (λ x4 . x1 x4),
x2,
x3,
∃ x4 . and (and (In x4 x0) (x1 x4)) (x3 = x2 x4) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x4 of type ι be given.
Assume H1:
In x4 (Sep x0 (λ x5 . x1 x5)).
Assume H2: x3 = x2 x4.
Apply unknownprop_6a6b356f855b99f3fbff4effcb62e3ee6aa23839e10650eb28a503a368c2bb09 with
x0,
x1,
x4,
∃ x5 . and (and (In x5 x0) (x1 x5)) (x3 = x2 x5) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H4: x1 x4.
Let x5 of type ο be given.
Assume H5:
∀ x6 . and (and (In x6 x0) (x1 x6)) (x3 = x2 x6) ⟶ x5.
Apply H5 with
x4.
Apply unknownprop_c7bf67064987d41cefc55afb6af6ecbbb6b830405f2005e0def6e504b3ca3bf3 with
In x4 x0,
x1 x4,
x3 = x2 x4 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H2.