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