Theorem: zero_eq_propagate (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
⊢ zeroSeq = propagate Empty.elim (fun x x => (Empty.elim, false)) Empty.elim
Tactic:
ext n
State after:
case h
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ zeroSeq n = propagate Empty.elim (fun x x => (Empty.elim, false)) Empty.elim n

State before:
case h
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ zeroSeq n = propagate Empty.elim (fun x x => (Empty.elim, false)) Empty.elim n
Tactic:
cases n <;> rfl
State after:
no goals