Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Claim L3: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Claim L4: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
set y9 to be λ x9 . x8
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x5,
y6,
λ x10 x11 . y9 (bc82c.. y4 x10) (bc82c.. y4 x11) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
set y8 to be λ x8 . y7
Apply L4 with
λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H5: y8 y7 y7.
The subproof is completed by applying H5.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with
x5,
y7,
y6,
λ x9 . y8 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
Claim L5: ∀ x11 : ι → ο . x11 y10 ⟶ x11 y9
Let x11 of type ι → ο be given.
set y12 to be λ x12 . x11
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
y7,
y9,
λ x13 x14 . y12 (bc82c.. x13 y8) (bc82c.. x14 y8) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
set y11 to be λ x11 . y10
Apply L5 with
λ x12 . y11 x12 y10 ⟶ y11 y10 x12 leaving 2 subgoals.
Assume H6: y11 y10 y10.
The subproof is completed by applying H6.
set y12 to be λ x12 . y11
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with
y10,
y8,
y9,
λ x13 x14 . y12 x14 x13 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying L5.
Let x5 of type ι → ι → ο be given.
Apply L3 with
λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H4: x5 y4 y4.
The subproof is completed by applying H4.