match n with
| 0 => rfl
| 1 => rfl
| n+2 => simp [lsSeq, propagate_succ]
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ lsSeq x n = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) n
no goals