-let eta_expand g tys t =
- assert (tys <> []);
- let name i = Printf.sprintf "%s%u" expanded_premise i in
- let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in
- let arg i = C.Rel (succ i) in
- let rec aux i f a = function
- | [] -> f, a
- | (_, ty) :: tl -> aux (succ i) (H.compose f (lambda i ty)) (arg i :: a) tl
- in
- let n = List.length tys in
- let absts, args = aux 0 H.identity [] tys in
- let t = match S.lift n t with
- | C.Appl ts -> C.Appl (ts @ args)
- | t -> C.Appl (t :: args)
- in
- g (absts t)
-
-let rec opt2_letin g c name v w t =
- let entry = Some (name, C.Def (v, w)) in
- let g t =
- let g v = g (C.LetIn (name, v, w, t)) in
- opt2_term g c v
- in
- opt2_proof g (entry :: c) t