-let rec beta_reduce =
- function
- (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
- let he'' = CicSubstitution.subst he' t in
- if tl' = [] then
- he''
- else
- beta_reduce (Cic.Appl(he''::tl'))
- | t -> t
-(*
-let rec deref subst =
- let snd (_,a,_) = a in
- function
- Cic.Meta(n,l) as t ->
- (try
- deref subst
- (CicSubstitution.subst_meta
- l (snd (CicUtil.lookup_subst n subst)))
- with
- CicUtil.Subst_not_found _ -> t)
- | t -> t
-;; *)
-