Let x0 of type ι be given.
Apply unknownprop_cce65446ff59911a5cd0f0aa52c7a372f2f1990c39bd3db3c9fd2ea818c2e216 with
x0,
λ x1 x2 . f4dc0.. x0 = 236dc.. (f4dc0.. x2) (f4dc0.. (f6a32.. x0)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_a7cae15d14a6e4791f91b3ea7ac5511c0d8df820499a97872d4161ec0acb2004 with
x0,
λ x1 x2 . f4dc0.. x0 = 236dc.. (f4dc0.. x0) (f4dc0.. x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_20f7c07c769e8e0463ee8d1144e160b5b270178e03c936033ca4568d83368a9c with
λ x1 x2 . f4dc0.. x0 = 236dc.. (f4dc0.. x0) x2.
Let x1 of type ι → ι → ο be given.
The subproof is completed by applying unknownprop_8caab58746e5d2d24e79c56b1fd1ad38271bed0128653f24088edadc36aa9114 with
f4dc0.. x0,
λ x2 x3 . x1 x3 x2.