/workspace/scratch/d3c8f9dc75d7/project/negative_controls/PositiveLiftMustBeStrict.lean:3:44: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  OfNat (Fin zeroBranchCertificate.fst) 0
numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
  Fin zeroBranchCertificate.fst
due to the absence of the instance above

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
/workspace/scratch/d3c8f9dc75d7/project/negative_controls/PositiveLiftMustBeStrict.lean:3:46: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  OfNat (Fin zeroBranchCertificate.fst) 0
numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
  Fin zeroBranchCertificate.fst
due to the absence of the instance above

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
/workspace/scratch/d3c8f9dc75d7/project/negative_controls/PositiveLiftMustBeStrict.lean:3:51: error: unsolved goals
⊢ False
