constant lit$year : (Str) constant lit$title : (Str) constant lit$star : (Str) constant lit$director : (Str) constant listElts : (func(0, [LLChar; (Set_Set Str)])) constant Set_sng : (func(1, [@(0); (Set_Set @(0))])) bind 1 a : {a : Str | a == "director" } bind 2 things : {v : LLChar | (listElts v ~~ (Set_cup (Set_sng lit$year) (Set_cup (Set_sng lit$star) (Set_cup (Set_sng lit$director) (Set_sng lit$title)))))} constraint: env [ 1; 2 ] lhs {v : int | true } rhs {v : int | Set_mem a (listElts things)} id 1 tag []