Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_6402afcf89af96ded942e84b9859aeeef4ba7eaef1979737905398451311e541 with
x0,
λ x2 . EquivReln (BinReln_product x2 x1) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Let x3 of type ι → ι → ο be given.
Assume H2: ∀ x4 . x4 ∈ x2 ⟶ x3 x4 x4.
Assume H3: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x4.
Assume H4: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6.
Apply unknownprop_6402afcf89af96ded942e84b9859aeeef4ba7eaef1979737905398451311e541 with
x1,
λ x4 . EquivReln (BinReln_product (pack_r x2 x3) x4) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Let x5 of type ι → ι → ο be given.
Assume H5: ∀ x6 . x6 ∈ x4 ⟶ x5 x6 x6.
Assume H6: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 x7 ⟶ x5 x7 x6.
Assume H7: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ ∀ x8 . x8 ∈ x4 ⟶ x5 x6 x7 ⟶ x5 x7 x8 ⟶ x5 x6 x8.
Apply unknownprop_efcdca50692a8e5dea3b2dabd19b7c98b28ec0cd127c886a2f9539f6c2a2ba01 with
x2,
x3,
x4,
x5,
λ x6 x7 . EquivReln x7.
Apply unknownprop_46185b99972d7cc500b0fcea77da3881e5aca4376b72d7aefbcc4420b07dadec with
setprod x2 x4,
λ x6 x7 . and (x3 (ap x6 0) (ap x7 0)) (x5 (ap x6 1) (ap x7 1)) leaving 3 subgoals.
Let x6 of type ι be given.
Apply andI with
x3 (ap x6 0) (ap x6 0),
x5 (ap x6 1) (ap x6 1) leaving 2 subgoals.
Apply H2 with
ap x6 0.
Apply ap0_Sigma with
x2,
λ x7 . x4,
x6.
The subproof is completed by applying H8.
Apply H5 with
ap x6 1.
Apply ap1_Sigma with
x2,
λ x7 . x4,
x6.
The subproof is completed by applying H8.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H10:
and (x3 (ap x6 0) (ap x7 0)) (x5 (ap x6 1) (ap x7 1)).
Apply H10 with
(λ x8 x9 . and (x3 (ap x8 0) (ap x9 0)) (x5 (ap x8 1) (ap x9 1))) x7 x6.
Assume H11:
x3 (ap x6 0) (ap x7 0).
Assume H12:
x5 (ap x6 1) (ap x7 1).
Apply andI with
x3 (ap x7 0) (ap x6 0),
x5 (ap x7 1) (ap x6 1) leaving 2 subgoals.
Apply H3 with
ap x6 0,
ap x7 0 leaving 3 subgoals.
Apply ap0_Sigma with
x2,
λ x8 . x4,
x6.
The subproof is completed by applying H8.
Apply ap0_Sigma with
x2,
λ x8 . x4,
x7.
The subproof is completed by applying H9.
The subproof is completed by applying H11.
Apply H6 with
ap x6 1,
ap x7 1 leaving 3 subgoals.