ext n
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
⊢ orSeq x y = propagate Empty.elim (fun x y => (Empty.elim, y true || y false)) fun b => bif b then x else y
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ orSeq x y n = propagate Empty.elim (fun x y => (Empty.elim, y true || y false)) (fun b => bif b then x else y) n