KP.fprintf och "Definition %a := %a.\n\n%!" out_uri u (out_term st false B.empty) v;
(* KP.fprintf och "Strategy -%u [ %a ].\n\n%!" na.E.n_apix out_uri u; *) !ok
| E.Abst w ->
KP.fprintf och "Definition %a := %a.\n\n%!" out_uri u (out_term st false B.empty) v;
(* KP.fprintf och "Strategy -%u [ %a ].\n\n%!" na.E.n_apix out_uri u; *) !ok
| E.Abst w ->