module E = CicEnvironment
module UM = UriManager
module D = Deannotate
+module PER = ProofEngineReduction
+module Ut = CicUtil
(* fresh name generator *****************************************************)
let cic = D.deannotate_term
+let occurs c ~what ~where =
+ let result = ref false in
+ let equality c t1 t2 =
+ let r = Ut.alpha_equivalence t1 t2 in
+ result := !result || r; r
+ in
+ let context, what, with_what = c, [what], [C.Rel 0] in
+ let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
+ !result
+
(* Ensuring Barendregt convenction ******************************************)
let rec add_entries map c = function