constant prop : func(2, [@(0); @(1)]) constant gibber : func(0, [int; int; int]) // constant prop : func(0, [Binary; Bin]) data Bin 0 = [ | mkBin { nBin : Int } ] data Binary 0 = [ | mkB0 { } | mkB1 { } ] bind 0 n : {n:Int | gibber 2 3 = 4 } bind 1 p : {p:Binary | prop p = mkBin n && prop p = mkBin 0} bind 2 p : {p:Binary | prop p = mkBin n && prop p = mkBin 1} constraint: env [0; 1] lhs {v:int | true} rhs {v:int | n == 0 || n == 1} id 1 tag [] constraint: env [0; 2] lhs {v:int | true} rhs {v:int | n == 0 } id 2 tag []