+
+let write_subst och n s =
+ Printf.fprintf och "%s %s\n" s n
+
+let rec write_fst och = function
+ | [] -> ()
+ | ET.Other (2, _, s, _) :: ET.Line _ :: ET.Text t :: tl ->
+ write_snd och tl s (EL.split_on_char ' ' t)
+ | ET.Other (2, _, s, _) :: tl ->
+ Printf.eprintf "skipping fst: %S\n" s;
+ write_fst och tl
+ | _ :: tl -> write_fst och tl
+
+and write_snd och tl s = function
+ | "definition" :: n :: _
+ | "fact" :: n :: _
+ | "lemma" :: n :: _
+ | "inductive" :: n :: _
+ | "theorem" :: n :: _ ->
+ let ss = EL.split_on_char ' ' s in
+ List.iter (write_subst och n) (List.tl ss);
+ write_fst och tl
+ | t :: _ ->
+ Printf.eprintf "skipping snd: %S %S\n" s t;
+ write_fst och tl
+ | [] ->
+ Printf.eprintf "skipping snd: %S\n" s;
+ write_fst och tl
+
+let write_substs = write_fst