+let existselim t id1 t1 id2 t2 =
+(*BUG: t1 and t2 not used *)
+(*PARSING BUG: t2 is parsed in the current context, but it may
+ have occurrences of id1 in it *)
+ Tactics.elim_intros t
+ ~mk_fresh_name_callback:
+ (let i = ref 0 in
+ fun _ _ _ ~typ ->
+ incr i;
+ if !i = 1 then Cic.Name id1 else Cic.Name id2)
+
+let andelim = existselim;;
+
+let rewritingstep ~dbd ~universe lhs rhs just last_step =
+ let aux ((proof,goal) as status) =
+ let (curi,metasenv,proofbo,proofty, attrs) = proof in
+ let _,context,gty = CicUtil.lookup_meta goal metasenv in
+ let eq,trans =
+ match LibraryObjects.eq_URI () with
+ None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
+ | Some uri ->
+ Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
+ in
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
+ let just =
+ match just with
+ `Auto params ->
+ let params =
+ if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
+ ("paramodulation","1")::params
+ else params in
+ let params =
+ if not (List.exists (fun (k,_) -> k = "timeout") params) then
+ ("timeout","3")::params
+ else params
+ in
+ Tactics.auto ~dbd ~params ~universe
+ | `Term just -> Tactics.apply just