match n with
| 0 => rfl
| 1 => rfl
| n+2 => simp [oneSeq, propagate_succ]
case h
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ oneSeq n = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim n
no goals