ext n
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
⊢ lsSeq x = propagate (fun x => false) (fun carry x => (x, carry ())) fun x_1 => x
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ lsSeq x n = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) n