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