bytecode:
  [start,true{7}][is,[_]][is,true]

type inference:
  [obj{0}, true{7}, [[obj{0}, true]], true{0,7}, true{0,7}]

obj{0}    : [start] is an initial function.
true{7}   : [start] range is known (the arguments of [start]).
true{0,7} : [is] filters if argument doesn't resolve to true (thus, quantifier lowsided at 0)


Important concepts:

  1. mm-ADT doesn't make a distinction between types and instances. true is an instance that can serve as a "type."
  2. with more intelligence on the semantics of [is] (not just that its a filter function), true{0,7} would be true{7}.