Theorem: LO.FirstOrder.UFormula.shiftb_zero (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
b : ℕ → UTerm L μ
⊢ shiftb b 0 = b
Tactic:
unfold shiftb
State after:
L : Language
μ : Type v
b : ℕ → UTerm L μ
⊢ (fun x => if x < 0 then UTerm.bvar x else UTerm.bShifts 0 (b (x - 0))) = b

State before:
L : Language
μ : Type v
b : ℕ → UTerm L μ
⊢ (fun x => if x < 0 then UTerm.bvar x else UTerm.bShifts 0 (b (x - 0))) = b
Tactic:
simp
State after:
no goals