val ho_whd:
(ho_whd_result -> 'a) -> Bag.context -> Bag.term -> 'a
val are_convertible:
(ac_result -> 'a) -> Bag.context -> Bag.term -> Bag.term -> 'a
val ho_whd:
(ho_whd_result -> 'a) -> Bag.context -> Bag.term -> 'a
val are_convertible:
(ac_result -> 'a) -> Bag.context -> Bag.term -> Bag.term -> 'a