α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
⊢ (∀ (n : ℕ), Terminates (get? s n)) ↔ ∀ (n : ℕ), Terminates (get? t n)
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
⊢ Productive s ↔ Productive t
simp only [productive_iff]
no goals
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
⊢ (∀ (n : ℕ), Terminates (get? s n)) ↔ ∀ (n : ℕ), Terminates (get? t n)
exact forall_congr' fun n => terminates_congr <| get?_congr h _