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_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with
x0,
x2,
equip (setprod x0 x1) (setprod x2 x3) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x4 of type ι → ι be given.
Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with
x0,
x2,
x4,
equip (setprod x0 x1) (setprod x2 x3) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with
x0,
x2,
x4,
(∀ x5 . In x5 x2 ⟶ ∃ x6 . and (In x6 x0) (x4 x6 = x5)) ⟶ equip (setprod x0 x1) (setprod x2 x3) leaving 2 subgoals.
The subproof is completed by applying H3.
Assume H4:
∀ x5 . In x5 x0 ⟶ In (x4 x5) x2.
Assume H5:
∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x0 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.
Assume H6:
∀ x5 . In x5 x2 ⟶ ∃ x6 . and (In x6 x0) (x4 x6 = x5).
Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with
x1,
x3,
equip (setprod x0 x1) (setprod x2 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x5 of type ι → ι be given.
Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with
x1,
x3,
x5,
equip (setprod x0 x1) (setprod x2 x3) leaving 2 subgoals.
The subproof is completed by applying H7.
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with
x1,
x3,
x5,
(∀ x6 . In x6 x3 ⟶ ∃ x7 . and (In x7 x1) (x5 x7 = x6)) ⟶ equip (setprod x0 x1) (setprod x2 x3) leaving 2 subgoals.
The subproof is completed by applying H8.
Assume H9:
∀ x6 . In x6 x1 ⟶ In (x5 x6) x3.
Assume H10:
∀ x6 . In x6 x1 ⟶ ∀ x7 . In x7 x1 ⟶ x5 x6 = x5 x7 ⟶ x6 = x7.
Assume H11:
∀ x6 . In x6 x3 ⟶ ∃ x7 . and (In x7 x1) (x5 x7 = x6).
Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with
setprod x0 x1,
setprod x2 x3,
λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (x4 (ap x6 0)) (x5 (ap x6 1))).
Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with
setprod x0 x1,
setprod x2 x3,
λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (x4 (ap x6 0)) (x5 (ap x6 1))) leaving 2 subgoals.
Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with
setprod x0 x1,
setprod x2 x3,
λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (x4 (ap x6 0)) (x5 (ap x6 1))) leaving 2 subgoals.
Let x6 of type ι be given.
Apply unknownprop_ca2474a6276e8f820c97f5b2341436efc5ee69afd93bd4fd7a8b330e27b79018 with
x2,
x3,
x4 ...,
... leaving 2 subgoals.