| By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^
(match term2 with None -> " " | Some term2 -> term_pp term2)
| We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
| By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^
(match term2 with None -> " " | Some term2 -> term_pp term2)
| We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1)