Let x0 of type ι be given.
Apply unknownprop_f8cb4609f9c174a593de5a10197e2915f5c1a2d9f32ed8d30c3d30b788bb9e1e with
λ x1 x2 : ι → ι → ι . x2 x0 x0 = setexp x0 2.
Apply unknownprop_9cbe1b438cb309fdaf3dcacebb3b572a10a17828098a582be8e9441d5a1eab25 with
λ x1 x2 : ι → ι → ι . (λ x3 x4 . lam x3 (λ x5 . x4)) x0 x0 = x2 x0 2.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
(λ x1 x2 . lam x1 (λ x3 . x2)) x0 x0,
(λ x1 x2 . Pi x2 (λ x3 . x1)) x0 2 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H0:
In x1 ((λ x2 x3 . lam x2 (λ x4 . x3)) x0 x0).
Apply unknownprop_1eb28f5831a9d21e218b89c238edbbf849d22045bb77ce7cec926a651d1793f0 with
setsum (proj0 x1) (proj1 x1) = x1,
In (proj0 x1) x0,
In (proj1 x1) x0,
In x1 ((λ x2 x3 . Pi x3 (λ x4 . x2)) x0 2) leaving 2 subgoals.
Apply unknownprop_632d5604ed3c6300a4762cec49c7927befabcc480df4aa1142cf8872f14519d7 with
x0,
λ x2 . x0,
x1.
The subproof is completed by applying H0.
Apply H1 with
λ x2 x3 . In x2 ((λ x4 x5 . Pi x5 (λ x6 . x4)) x0 2).
Apply unknownprop_185bdf858edd42f8afc761ae1953b80df75013886328f1ada27b2892070076d1 with
proj0 x1,
proj1 x1,
λ x2 x3 . In x3 (Pi 2 (λ x4 . x0)).
Apply unknownprop_ae7ff6762664969563026849f911ad347655d2dee93f3e04751eb40cfcd41ed9 with
2,
λ x2 . x0,
λ x2 . If_i (x2 = 0) (proj0 x1) (proj1 x1).
Let x2 of type ι be given.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
If_i (x2 = 0) (proj0 x1) (proj1 x1) = proj0 x1,
If_i (x2 = 0) (proj0 x1) (proj1 x1) = proj1 x1,
In (If_i (x2 = 0) (proj0 x1) (proj1 x1)) x0 leaving 3 subgoals.
The subproof is completed by applying unknownprop_5870882cb2ad83e503e81806c30f735b1750ff9c431d2bf0bc24cc0e00611bf5 with
x2 = 0,
proj0 x1,
proj1 x1.
Apply H5 with
λ x3 x4 . In x4 x0.
The subproof is completed by applying H2.
Apply H5 with
λ x3 x4 . In x4 x0.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H0:
In x1 ((λ x2 x3 . Pi x3 (λ x4 . x2)) x0 2).
Apply unknownprop_c20579f7ec03c9b411c1afcdcbd6eb7f887b4dea35b13dd2fe5a71172b6554fe with
2,
λ x2 . x0,
x1,
In x1 ((λ x2 x3 . lam x2 (λ x4 . x3)) x0 x0) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H2:
∀ x2 . In x2 2 ⟶ In (ap x1 x2) x0.
Apply L3 with
λ x2 x3 . In x2 ((λ x4 x5 . lam x4 (λ x6 . x5)) x0 x0).
Apply unknownprop_1633a25a08ee627a1613041ad1ebe0a4535d0c6ce109cb609e7d9a519dad2f25 with
x0,
λ x2 . x0,
ap x1 0,
ap x1 1 leaving 2 subgoals.