+ in let u' = unit_dpm (q obj)
+ in u' (r, h)
+ ) else unit_dpm false
+ in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+ -->
+
+ let eliminator = fun truth_value ->
+ if truth_value
+ then (fun (r, h) ->
+ let obj = List.nth h (r 'x')
+ in (q obj, r, h)
+ ) else unit_dpm false
+ in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+
+ This is a function that takes a `bool dpm` as input and returns a `bool dpm set` as output.
+
+ (Compare to the \[[Qx]] we had before: