inductive t2_eqv (rhs : Rego.Any) : Prop
| rule₁ : (let x := 42
           let y := 41
           x > y) →
          (rhs = Rego.Any.bool true) →
          t2_eqv rhs

-- Alternative form where the parameters are unnamed.

inductive t2_eqv' : Bool → Prop
| rule₁ : (let x := 42
           let y := 41
           x > y) →
          t2_eqv' true