Boole: datatype tester incorrectly resolves as free variable

[ChengZ3]

When a Boole program contains 4+ datatype declarations and the first datatype has constructor testers referenced by a later function, the verifier reports those tester references as Free Variables during type-check, even though the datatype is fully declared earlier. The issue disappears when the referenced datatype is not the first one. Also, the same program structure verifies without error when written as a Core program.

datatype_fails.lean — fails type-check

/-
  Differs from `datatype_fails.lean` only in the position of `color`:
  here it appears FIRST (position 0); there it appears at position 1.

  Expected:
  ❌ Type checking error.
  [assert [get_val_body_calls_color..color_Red_0_0] ((~Bool.Implies : (arrow bool (arrow bool bool)))
   (color..iscolor_Red c)
   (~color..iscolor_Red c))] No free variables are allowed here!
  Free Variables: [color..iscolor_Red]
-/

import Strata.MetaVerifier

open Strata

private def datatype_fails_program : Strata.Program :=
#strata
program Boole;

 datatype color {
  color_Red(color_Red_0 : int),
  color_Blue(color_Blue_0 : int)
};
 datatype tag1 {
  tag1_only()
};
 datatype tag2 {
  tag2_only()
};
 datatype tag3 {
  tag3_only()
};
 function get_val (c : color) : int {
  if color..iscolor_Red(c) then color..color_Red_0(c) else color..color_Blue_0(c)
}
#end

#eval Strata.Boole.verify "cvc5" datatype_fails_program (options := .quiet)

datatype_passes.lean — same body, color moved to after tag1

/-
  Expected:
  Obligation: get_val_body_calls_color..color_Red_0_0
  Property: assert
  Result: ✅ pass
  
  Obligation: get_val_body_calls_color..color_Blue_0_1
  Property: assert
  Result: ✅ pass
-/

import Strata.MetaVerifier

open Strata

private def datatype_passes_program : Strata.Program :=
#strata
program Boole;

 datatype tag1 {
  tag1_only()
};
 datatype color {
  color_Red(color_Red_0 : int),
  color_Blue(color_Blue_0 : int)
};
 datatype tag2 {
  tag2_only()
};
 datatype tag3 {
  tag3_only()
};
 function get_val (c : color) : int {
  if color..iscolor_Red(c) then color..color_Red_0(c) else color..color_Blue_0(c)
}
#end

#eval Strata.Boole.verify "cvc5" datatype_passes_program (options := .quiet)