+
+
+let term_of_equality equality =
+ let _, _, (ty, left, right, _), menv, args = equality in
+ let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
+ let argsno = List.length args in
+ let t =
+ CicSubstitution.lift argsno
+ (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+ in
+ snd (
+ List.fold_right
+ (fun a (n, t) ->
+ match a with
+ | Cic.Meta (i, _) ->
+ let name = Cic.Name ("X" ^ (string_of_int n)) in
+ let _, _, ty = CicUtil.lookup_meta i menv in
+ let t =
+ ProofEngineReduction.replace
+ ~equality:eq ~what:[i]
+ ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
+ in
+ (n-1, Cic.Prod (name, ty, t))
+ | _ -> assert false)
+ args (argsno, t))
+;;