Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι → ο be given.
Let x3 of type ι be given.
Apply unknownprop_4f2a2369eaded4c9b63034283fc58b51368538c62861e5afabd055ffcc38610f with
λ x4 x5 : ι → (ι → ι) → (ι → ι → ο) → ι . In x3 (x5 x0 x1 x2) ⟶ ∀ x6 : ι → ο . (∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 (x1 x7) ⟶ x2 x7 x8 ⟶ x6 (lam 2 (λ x9 . If_i (x9 = 0) x7 x8))) ⟶ x6 x3.
Assume H0:
In x3 ((λ x4 . λ x5 : ι → ι . λ x6 : ι → ι → ο . Sep (lam x4 x5) (λ x7 . x6 (ap x7 0) (ap x7 1))) x0 x1 x2).
Let x4 of type ι → ο be given.
Assume H1:
∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 (x1 x5) ⟶ x2 x5 x6 ⟶ x4 (lam 2 (λ x7 . If_i (x7 = 0) x5 x6)).
Apply unknownprop_6a6b356f855b99f3fbff4effcb62e3ee6aa23839e10650eb28a503a368c2bb09 with
lam x0 (λ x5 . x1 x5),
λ x5 . x2 (ap x5 0) (ap x5 1),
x3,
x4 x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H2:
In x3 (lam x0 (λ x5 . x1 x5)).
Apply unknownprop_b0f45156a07c806d581dec43db7a09d24fa0b4ffd05ff6113989de6fa6a96f93 with
x0,
x1,
x3,
λ x5 . x2 (ap x5 0) (ap x5 1) ⟶ x4 x5 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H4:
In x6 (x1 x5).
Apply unknownprop_ab640183089126bd192ea777bf3d0693f7fc019527e86171644bd6e54256c0e4 with
x5,
x6,
λ x7 x8 . x2 x8 (ap (lam 2 (λ x9 . If_i (x9 = 0) x5 x6)) 1) ⟶ x4 (lam 2 (λ x9 . If_i (x9 = 0) x5 x6)).
Apply unknownprop_c08558c9c7b6c1be6215b272fb7932c68e2862a19045743bcd34753544c4d493 with
x5,
x6,
λ x7 x8 . x2 x5 x8 ⟶ x4 (lam 2 (λ x9 . If_i (x9 = 0) x5 x6)).
Apply H1 with
x5,
x6 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.