qualif Sz(v: Tree): (0 < thinginess v)
qualif Sz(v: Tree): (1 < 0)

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 }