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_4e4d5268bbb87fe215de6332b7fe34a72fc7e7399afc4b12f4dd64f0c1ba7afe with
x0,
x1,
x2,
λ x4 x5 . In x4 (setexp x3 3).
Apply unknownprop_9cbe1b438cb309fdaf3dcacebb3b572a10a17828098a582be8e9441d5a1eab25 with
λ x4 x5 : ι → ι → ι . In (lam 3 (ap (lam 3 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 x2))))) (x5 x3 3).
Apply unknownprop_ae7ff6762664969563026849f911ad347655d2dee93f3e04751eb40cfcd41ed9 with
3,
λ x4 . x3,
λ x4 . ap (lam 3 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 x2))) x4.
Let x4 of type ι be given.
Apply unknownprop_f20f08b38429d0914c6a2c13ffdd3fa446ab4342ea7a43d47915b2eca12847ee with
x4,
λ x5 . In (ap (lam 3 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 x2))) x5) x3 leaving 4 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_72ee6a4729e4d36966f7c731b465de1ffff5565146924f50f9d4e56e3e4f5133 with
x0,
x1,
x2,
λ x5 x6 . In x6 x3.
The subproof is completed by applying H0.
Apply unknownprop_ad0347fd00c465af5dfdd914ea5ee88ed02126a7c7ef66823f6c720d34ff7b99 with
x0,
x1,
x2,
λ x5 x6 . In x6 x3.
The subproof is completed by applying H1.
Apply unknownprop_8a884b2bd6ff36eba8856072c2baa52cff32d5e85b68403b704927d5d62d4773 with
x0,
x1,
x2,
λ x5 x6 . In x6 x3.
The subproof is completed by applying H2.