import Lean.Data.Json

inductive pi_eqv (n : Rego.Any) : Prop
| rule₁ : (∃ (x : Lean.JsonNumber), x = 3.14159 ∧ (n = Rego.Any.num x)) →
          pi_eqv n

def pi : Lean.JsonNumber := 3.14159

theorem def_pi_correct : pi_eqv (Rego.Any.num pi) := by
  apply pi_eqv.rule₁
  exists pi