+
+and transitivity
+ seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
+=
+ let module C2A = Cic2acic in
+ let module K = Content in
+ let module C = Cic in
+ match li with
+ | C.AConst (sid,uri,exp_named_subst)::args
+ when LibraryObjects.is_trans_eq_URI uri ->
+ let exp_args = List.map snd exp_named_subst in
+ let t1,t2,t3,p1,p2 =
+ match exp_args@args with
+ | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
+ | _ -> raise NotApplicable
+ in
+ { K.proof_name = name;
+ K.proof_id = gen_id proof_prefix seed;
+ K.proof_context = [];
+ K.proof_apply_context = [];
+ K.proof_conclude =
+ { K.conclude_id = gen_id conclude_prefix seed;
+ K.conclude_aref = id;
+ K.conclude_method = "Eq_chain";
+ K.conclude_args =
+ K.Term (false,t1)::
+ (transitivity_aux
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1)
+ @ [K.Term (false,t2)]@
+ (transitivity_aux
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2)
+ @ [K.Term (false,t3)];
+ K.conclude_conclusion =
+ try Some
+ (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+ with Not_found -> None
+ }
+ }
+ | _ -> raise NotApplicable
+
+and transitivity_aux seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts t =
+ let module C2A = Cic2acic in
+ let module K = Content in
+ let module C = Cic in
+ match t with
+ | C.AAppl (_,C.AConst (sid,uri,exp_named_subst)::args)
+ when LibraryObjects.is_trans_eq_URI uri ->
+ let exp_args = List.map snd exp_named_subst in
+ let t1,t2,t3,p1,p2 =
+ match exp_args@args with
+ | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
+ | _ -> raise NotApplicable
+ in
+ (transitivity_aux
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1)
+ @[K.Term (false,t2)]
+ @(transitivity_aux
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2)
+ | _ -> [K.ArgProof
+ (acic2content seed context metasenv ~ids_to_inner_sorts ~ids_to_inner_types t)]
+