Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_ded7318fe13a7765a9fe494f98a83e2ddbc6dd175169198d79ca7734476d72a7 with
λ x2 x3 . 0,
λ x2 . λ x3 : ι → ι → ι . λ x4 x5 . b38a5.. (ap x4 0) (ap x5 0) (x3 (stream_rest x4) (stream_rest x5)),
λ x2 x3 : ι → ι → ι . x3 x0 x1 = 0.
Let x2 of type ι → ι → ο be given.
Assume H0: x2 ((λ x3 x4 . 0) x0 x1) 0.
The subproof is completed by applying H0.