+ B.b_space; justif1])::
+ match justif2 with None -> [] | Some j -> [B.indent j])
+ else if conclude.Con.conclude_method = "Eq_chain" then
+ let justification p =
+ 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))::(aux tl)
+ | _ -> assert false
+ in
+ let hd =
+ match List.hd conclude.Con.conclude_args with
+ | Con.Term t -> t
+ | _ -> assert false
+ in
+ B.HOV([],[term2pres hd; (* B.b_space; *)
+ B.V ([],aux (List.tl conclude.Con.conclude_args))])