[qed] removing lc_empty and lc_closed_at

src/plugins/qed/logic.ml

@@ -367,12 +367,7 @@ sig
 
   (** {3 Locally Nameless Representation} *)
 
-  val lc_empty : term -> bool (** No bound variables *)
   val lc_closed : term -> bool (** All bound variables are under their binder *)
-  val lc_closed_at : int -> term -> bool
-  (** [lc_closed_at n] do not contains bvar with [k < n].
-      Means that the term has no bound-variable that can escape [n] binders
-      uppon the term. *)
 
   val lc_vars : term -> Bvars.t
 

src/plugins/qed/term.ml

@@ -1966,7 +1966,6 @@ struct
   (* --- Locally Nameless                                                   --- *)
   (* -------------------------------------------------------------------------- *)
 
-  let lc_empty e = Bvars.is_empty e.bind
   let lc_closed e = Bvars.closed e.bind
   let lc_closed_at n e = Bvars.closed_at n e.bind
   let lc_vars e = e.bind