- | C.ARel (_, _, _, binder) -> rewrite binder
- | _ -> assert false
-
-(*
- assert (get_inner_sort st where = `Prop);
- let pred, old = List.nth tl 2, List.nth tl 1 in
- let pred_name = defined_premise in
- let pred_text = "extracted" in
- let p1 = T.LetIn (pred_name, pred, pred_text) in
- let cut_name = assumed_premise in
- let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in
- let cut_text = "" in
- let p2 = T.Cut (cut_name, cut_type, cut_text) in
- let qs = [rewrite cut_name; mk_proof (next st) where] in
- [T.Branch (qs, ""); p2; p1]
-*)
+ | C.ARel (_, _, _, premise) ->
+ let script, what = mk_atomic st dtext what in
+ T.Rewrite (direction, what, Some (premise, name), dtext) :: script
+ | _ -> assert false
+