+ in let u' = dpm_unit (q obj)
+ in u' (r, h)
+ ) else dpm_unit false
+ in fun one_dpm -> set_unit (dpm_bind 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 dpm_unit false
+ in fun one_dpm -> set_unit (dpm_bind 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: