+ | Relation (_,id,a,aeq,refl,sym,trans) ->
+ "relation " ^ term_pp aeq ^ " on " ^ term_pp a ^
+ (match refl with
+ Some r -> " reflexivity proved by " ^ term_pp r
+ | None -> "") ^
+ (match sym with
+ Some r -> " symmetry proved by " ^ term_pp r
+ | None -> "") ^
+ (match trans with
+ Some r -> " transitivity proved by " ^ term_pp r
+ | None -> "")