Object obj1, obj2, obj3
Succ(obj1, obj2)
Succ(obj2, obj3)

forall Object obj {
  -- draw a circle with a text in it
  obj.y = 0
  obj.x = ?
  Circle {
    center: [obj.x, obj.y]
  }
  Text {
    string: nameof obj
    center: [obj.x, obj.y]
  }
}

forall Object o1, o2
where Succ(o1, o2) {
  -- o1 should be on the left of o2
  ensure o1.x < o2.x
}

Object obj1, obj2, obj3
Index(0, obj1)
Index(1, obj2)
Index(2, obj3)

forall Object obj1, obj2; Number n1; n2
where Index(n1, obj1); Index(n2, obj2) {
  -- reason about `n1` and `n2` within this block
  -- but this block is always going to get matched
}

forall Object obj1, obj2; Number n1, n2
where Index(n1, obj1); Index(n2, obj2); n1 < n2 {
  ensure obj1.x < obj2.x
}