+ B.b_space; justif1])::
+ match justif2 with None -> [] | Some j -> [B.indent j])
+*) B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (previous)."]); B.b_kw "by _"])
+ 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.Text ([],"conclude");B.b_space;term2pres hd; (* B.b_space; *)
+ B.V ([],aux (List.tl conclude.Con.conclude_args))])