-let u = CicUniv.empty_ugraph in
-prerr_endline ("XXXX rewrite<-: " ^ CicPp.ppterm (fst (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1 ; t2]) u)));
-prerr_endline ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1 ; t2])) ;
-prerr_endline ("XXXX equri: " ^ U.string_of_uri equri) ;
-prerr_endline ("XXXX tty : " ^ CicPp.ppterm tty) ;
-prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ;
-prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ;
-if (fst (CicTypeChecker.type_of_aux' metasenv' context' t1 u)) <> tty then
-prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst (CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ;
-if (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u)) <> tty then
-prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ;
-if (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u)) <>
-(fst (CicTypeChecker.type_of_aux' metasenv' context' t2 u))
- then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ; prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ;
-prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' term u)));