+ B.b_space; justif1])::
+ match justif2 with None -> [] | Some j -> [B.indent j])
+*)
+ if (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
+ || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down) then
+ B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term1 ; B.b_kw "=" ; term2; B.b_kw ") (equality)."]); B.b_kw "by _"])
+ else
+ B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (equality)."]); B.b_kw "by _"])
+(*CSC: bad idea
+ B.V([], [B.H([],[B.b_kw "obtain fooo " ; term2 ; B.b_kw "=" ; term1; B.b_kw "by" ; B.b_kw "proof" ; B.Text([],"."); justif1])]) *)
+ else if conclude.Con.conclude_method = "Eq_chain" then
+ let justification p =
+(*
+ if skip_initial_lambdas <> None (* cheating *) then
+ [B.b_kw "by _"]
+ else
+*)
+ let j1,j2 = justification term2pres p in
+ j1 :: B.b_space :: (match j2 with Some j -> [j] | None -> [])
+ in
+ let rec aux args =
+ match args with
+ | [] -> []
+ | (Con.ArgProof p)::(Con.Term (_,t))::tl ->
+ B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw
+ "=";B.b_space;term2pres t;B.b_space]@justification p@
+ (if tl <> [] then [B.Text ([],".")] else [])))::(aux tl)
+ | _ -> assert false
+ in
+ let hd =
+ match List.hd conclude.Con.conclude_args with
+ | Con.Term (_,t) -> t
+ | _ -> assert false
+ in
+ B.HOV([],[B.b_kw "conclude";B.b_space;term2pres hd; (* B.b_space; *)
+ B.V ([],aux (List.tl conclude.Con.conclude_args))])