cases decide (i<k) <;> simp [f_stable]
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ (decide (i < k) && f (getBit m i) (getBit n i)) = f (decide (i < k) && getBit m i) (decide (i < k) && getBit n i)
no goals