-let eta_expand n t =
- let id = Ut.id_of_annterm t in
- let ty = C.AImplicit ("", None) in
- let name i = Printf.sprintf "%s%u" expanded_premise i in
- let lambda i t = C.ALambda (id, C.Name (name i), ty, t) in
- let arg i n = T.mk_arel (n - i) (name (n - i - 1)) in
- let rec aux i f a =
- if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
- in
- let absts, args = aux 0 identity [] in
- match Cn.lift 1 n t with
- | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args))
- | t -> absts (C.AAppl ("", t :: args))
-
-let appl_expand n = function
- | C.AAppl (id, ts) ->
- let before, after = T.list_split (List.length ts + n) ts in
- C.AAppl (id, C.AAppl ("", before) :: after)
- | _ -> assert false
-