/-
  Generated by lsc — Lean types and pure function mirrors.
-/
import LemmaScript

namespace Pure

def occOf (arr : Array Int) (x : Int) (n : Nat) : Int :=
  if n = 0 then
    0
  else
    occOf arr x (n - 1) + (if arr[n - 1]! = x then 1 else 0)
termination_by n

end Pure