case zero
M : Type u_1
inst✝ : Semigroup M
a✝ a : Stream' M
⊢ Stream'.nth a Nat.zero ∈ FP a

case succ
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
i : ℕ
ih : ∀ (a : Stream' M), Stream'.nth a i ∈ FP a
a : Stream' M
⊢ Stream'.nth a (Nat.succ i) ∈ FP a
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i : ℕ
⊢ Stream'.nth a i ∈ FP a
induction' i with i ih generalizing a
no goals
case zero
M : Type u_1
inst✝ : Semigroup M
a✝ a : Stream' M
⊢ Stream'.nth a Nat.zero ∈ FP a
apply FP.head
case succ.h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
i : ℕ
ih : ∀ (a : Stream' M), Stream'.nth a i ∈ FP a
a : Stream' M
⊢ FP (Stream'.tail a) (Stream'.nth a (Nat.succ i))
case succ
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
i : ℕ
ih : ∀ (a : Stream' M), Stream'.nth a i ∈ FP a
a : Stream' M
⊢ Stream'.nth a (Nat.succ i) ∈ FP a
apply FP.tail
no goals
case succ.h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
i : ℕ
ih : ∀ (a : Stream' M), Stream'.nth a i ∈ FP a
a : Stream' M
⊢ FP (Stream'.tail a) (Stream'.nth a (Nat.succ i))
apply ih