定理証明支援系Coqを用いた証明スクリプトは，手続き型の記述が成されるので可読性が高いとは言い難く，証明の全体構造の把握は容易とは限らない．証明の可読性向上には図示ツールが有効であると考えられる．ProofGeneralと連携した証明木描画ツールを拡張したTrafは，証明の全体構造の俯瞰的な把握に適した情報量の証明木を提示する．我々は．大域的及び局所的な観点からTrafの改良を試みている．本発表では，大きく広がりがちな証明木をコンパクトに表示するための工夫に加え，局所的に生成されるラベルの有効範囲の明示により証明ステップの詳細を把握しやすくしたGUIの設計と実装について報告する．