| AndElim (_, term, ident1, term1, ident2, term2) -> "by " ^ term_pp term ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")"
| RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | `Term term2 -> term_pp term2) ^ (if cont then " done" else "")
| Case (_, id, args) ->
| AndElim (_, term, ident1, term1, ident2, term2) -> "by " ^ term_pp term ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")"
| RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | `Term term2 -> term_pp term2) ^ (if cont then " done" else "")
| Case (_, id, args) ->