ext n
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
⊢ notSeq x = propagate Empty.elim (fun x y => (Empty.elim, !y ())) fun x_1 => x
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ notSeq x n = propagate Empty.elim (fun x y => (Empty.elim, !y ())) (fun x_1 => x) n