let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
(* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *)
let params = List.map (fun x -> NTactics.intro_tac ("a" ^ string_of_int x)) nlist in
let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
(* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *)
let params = List.map (fun x -> NTactics.intro_tac ("a" ^ string_of_int x)) nlist in