Apply unknownprop_7c3b12ad88949157af82dc8c8748a64e6f65ed820304dd6eff47f86adec1d200.
Apply unknownprop_acde72e2f50237aebb3f280c9adbd840002728dc66b42dda2437acbece7fe515 with
λ x0 . 236c6..,
λ x0 . prim1 (λ x1 . x0).
The subproof is completed by applying H0.
Apply L1 with
λ x0 x1 : ι → ι . (λ x2 . 236c6..) 236c6.. = x0 236c6...
Let x0 of type ι → ι → ο be given.
The subproof is completed by applying H2.