Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_ee6ce5840847ce6b33fd2ab8635c6f4d1cc75cd1ba9d2f744ef438b81a42e563 with
λ x3 x4 . 0,
λ x3 . λ x4 : ι → ι → ι . λ x5 x6 . b38a5.. (ap x5 0) (ap x6 0) (x4 (stream_rest x5) (stream_rest x6)),
x0,
λ x3 x4 : ι → ι → ι . x4 x1 x2 = b38a5.. (ap x1 0) (ap x2 0) (df9be.. x0 (stream_rest x1) (stream_rest x2)) leaving 2 subgoals.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.
Let x3 of type ι → ι → ο be given.
The subproof is completed by applying H1.