liquid-fixpoint-0.9.2.5: tests/pos/meas00.fq

fixpoint "--eliminate=some"

constant thinginess : func(0, [Tree; int])

constraint:
  env [ ]
  lhs {v : Tree | 666 < thinginess v }
  rhs {v : Tree | $k1  }
  id 1 tag []


constraint:
  env [ ]
  lhs {v : Tree | $k1  }
  rhs {v : Tree | 0 < thinginess v }
  id 2 tag []

wf:
  env [ ]
  reft { v: Tree | $k1 }