pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq)));
let dbranch it ~use_jmeq leftno consno =
pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq)));
let dbranch it ~use_jmeq leftno consno =
pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno));
let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
(* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *)
pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno));
let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
(* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *)