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_d158dd0ee7cd129998fef286b8e8d5798d9fdd1daf331b8339c3836f8066dce4 with
x0,
x1,
x2,
x3,
MetaCat x0 (λ x4 x5 . x1 x5 x4) x2 (λ x4 x5 x6 x7 x8 . x3 x6 x5 x4 x8 x7) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: ∀ x4 . x0 x4 ⟶ x1 x4 x4 (x2 x4).
Assume H2: ∀ x4 x5 x6 x7 x8 . x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x1 x4 x5 x7 ⟶ x1 x5 x6 x8 ⟶ x1 x4 x6 (x3 x4 x5 x6 x8 x7).
Assume H3: ∀ x4 x5 x6 . x0 x4 ⟶ x0 x5 ⟶ x1 x4 x5 x6 ⟶ x3 x4 x4 x5 x6 (x2 x4) = x6.
Assume H4: ∀ x4 x5 x6 . x0 x4 ⟶ x0 x5 ⟶ x1 x4 x5 x6 ⟶ x3 x4 x5 x5 (x2 x5) x6 = x6.
Assume H5: ∀ x4 x5 x6 x7 x8 x9 x10 . x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x1 x4 x5 x8 ⟶ x1 x5 x6 x9 ⟶ x1 x6 x7 x10 ⟶ x3 x4 x5 x7 (x3 x5 x6 x7 x10 x9) x8 = x3 x4 x6 x7 x10 (x3 x4 x5 x6 x9 x8).
Apply unknownprop_fc5379bc4ad65dc1954d6f65361b9d804f439ab0844013155adf361a615275a6 with
x0,
λ x4 x5 . x1 x5 x4,
x2,
λ x4 x5 x6 x7 x8 . x3 x6 x5 x4 x8 x7 leaving 5 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Assume H6: x0 x4.
Assume H7: x0 x5.
Assume H8: x0 x6.
Assume H9: x1 x5 x4 x7.
Assume H10: x1 x6 x5 x8.
Apply H2 with
x6,
x5,
x4,
x8,
x7 leaving 5 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H7.
The subproof is completed by applying H6.
The subproof is completed by applying H10.
The subproof is completed by applying H9.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H6: x0 x4.
Assume H7: x0 x5.
Assume H8: (λ x7 x8 . x1 x8 x7) x4 x5 x6.
Apply H4 with
x5,
x4,
x6 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H6: x0 x4.
Assume H7: x0 x5.
Assume H8: (λ x7 x8 . x1 x8 x7) x4 x5 x6.
Apply H3 with
x5,
x4,
x6 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Let x9 of type ι be given.
Let x10 of type ι be given.
Assume H6: x0 x4.
Assume H7: x0 x5.
Assume H8: x0 x6.
Assume H9: x0 x7.
Assume H10: (λ x11 x12 . x1 x12 x11) x4 x5 x8.
Assume H11: (λ x11 x12 . x1 x12 x11) x5 x6 x9.
Assume H12: (λ x11 x12 . x1 ... ...) ... ... ....