Theorem: PropagateStruc.eval_or (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ eval or x = orSeq (x true) (x false)
Tactic:
ext n
State after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n : ℕ
⊢ eval or x n = orSeq (x true) (x false) n

State before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n : ℕ
⊢ eval or x n = orSeq (x true) (x false) n
Tactic:
cases n <;> simp [or, orSeq, eval, propagate_succ]
State after:
no goals