- maxmeta := newmeta;
- newequality
- in
- let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
- and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
- and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
- and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
- let ok = function
- | _, (_, left, right), _, _ ->
- not (fst (CR.are_convertible context left right ugraph))
- in
- !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
+ let newmetas = newmetas @ newm' in
+ let newargs = args @ args' in
+ let build_new what other is_left eq_URI (t, s, m, ug) =
+ (* let what, other = *)
+ (* if is_left then left, right *)
+ (* else right, left *)
+ (* in *)
+ let newterm, neweqproof =
+ match t with
+ | C.Lambda (nn, ty, bo) ->
+ let bo' = M.apply_subst s (S.subst other bo) in
+ let bo'' =
+ C.Appl (
+ [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
+ if is_left then [bo'; S.lift 1 right]
+ else [S.lift 1 left; bo'])
+ in
+ let t' = C.Lambda (nn, ty, bo'') in
+ bo',
+ M.apply_subst s
+ (C.Appl [C.Const (eq_URI, []); ty; what; t';
+ eqproof; other; eqp'])
+ | _ -> assert false
+ in
+ let newmeta, newequality =
+ let left, right =
+ if is_left then (newterm, M.apply_subst s right)
+ else (M.apply_subst s left, newterm) in
+ fix_metas !maxmeta
+ (neweqproof, (eq_ty, left, right), newmetas, newargs)
+ in
+ maxmeta := newmeta;
+ newequality
+ in
+ let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
+ and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
+ and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
+ and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
+ let ok = function
+ | _, (_, left, right), _, _ ->
+ not (fst (CR.are_convertible context left right ugraph))
+ in
+ !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
+;;
+
+
+let is_identity ((_, context, ugraph) as env) = function
+ | ((_, (ty, left, right), _, _) as equality) ->
+ let res =
+ (left = right ||
+ (fst (CicReduction.are_convertible context left right ugraph)))
+ in
+(* if res then ( *)
+(* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
+(* print_newline (); *)
+(* ); *)
+ res