Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_c1d3826129d2eb54a8f1e40a6116497a0cdb00a6ee455a0b01d56d09477d50d0 with
x0,
λ x2 . PER (BinReln_exp 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 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x4.
Assume H3: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6.
Apply unknownprop_c1d3826129d2eb54a8f1e40a6116497a0cdb00a6ee455a0b01d56d09477d50d0 with
x1,
λ x4 . PER (BinReln_exp (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 H4: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 x7 ⟶ x5 x7 x6.
Assume H5: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ ∀ x8 . x8 ∈ x4 ⟶ x5 x6 x7 ⟶ x5 x7 x8 ⟶ x5 x6 x8.
Apply unknownprop_96b4efd33e0eab34902b0210050a90e84d3feb02930f35613e1732b2c4e43b01 with
x2,
x3,
x4,
x5,
λ x6 x7 . PER x7.
Apply unknownprop_b2515235786361aea7c15ac6711d5751cd13b11988163a3b347abdb56aff828a with
setexp x4 x2,
λ x6 x7 . ∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x2 ⟶ x3 x8 x9 ⟶ x5 (ap x6 x8) (ap x7 x9) leaving 2 subgoals.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H8:
∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x2 ⟶ x3 x8 x9 ⟶ x5 (ap x6 x8) (ap x7 x9).
Let x8 of type ι be given.
Assume H9: x8 ∈ x2.
Let x9 of type ι be given.
Assume H10: x9 ∈ x2.
Assume H11: x3 x8 x9.
Apply H4 with
ap x6 x9,
ap x7 x8 leaving 3 subgoals.
Apply ap_Pi with
x2,
λ x10 . x4,
x6,
x9 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H10.
Apply ap_Pi with
x2,
λ x10 . x4,
x7,
x8 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H9.
Apply H8 with
x9,
x8 leaving 3 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H9.
Apply H2 with
x8,
x9 leaving 3 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Assume H9:
∀ x9 . x9 ∈ x2 ⟶ ∀ x10 . x10 ∈ x2 ⟶ x3 x9 x10 ⟶ x5 (ap x6 x9) (ap x7 x10).
Assume H10:
∀ x9 . x9 ∈ x2 ⟶ ∀ x10 . x10 ∈ x2 ⟶ x3 x9 x10 ⟶ x5 (ap x7 x9) (ap x8 x10).
Let x9 of type ι be given.
Assume H11: x9 ∈ x2.
Let x10 of type ι be given.
Assume H12: x10 ∈ x2.
Assume H13: x3 x9 x10.
Apply H5 with
ap x6 x9,
ap x7 x9,
ap x8 x10 leaving 5 subgoals.
Apply ap_Pi with
x2,
λ x11 . ...,
...,
... leaving 2 subgoals.