Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x1 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply unknownprop_1030b2f82370682da82bd2e49c05e6c78943595f102389be16df3b42b6279cb8 with
x0,
x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 = x1 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x0 = x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H2: (λ x2 x3 . x0 x2 x2 x2 x2 x2 x2 x2 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3) = λ x2 x3 . x2.
Apply unknownprop_0bdc9214f3d13da435022f8588b958836c09a818ca32d79d0900f54c8d2527a2 with
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Assume H2: (λ x2 x3 . x0 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x2 x2 x2 x2) = λ x2 x3 . x2.
Apply unknownprop_c8f4c6132c330d292a33ed857f1378dfa11f59a06ab198d38d5ce3df4b16ca8f with
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.