# I found some very nice looking well structured proof, but I can't find a way create my own in that style

I found this very nice looking way to display equational proofs. It is used by Vene Vermo several times in his papers and I am wondering how to recreate it. When selecting things in the pdf I found that the vertical bars are lots of separate characters, I have no other clues.

• Welcome to TeX.SE. Please edit your posting to show us what you've tried so far and to note where you're experiencing difficulties. – Mico Oct 12 at 10:05

It can be obtained with two nested align(ed)at environments:

    \documentclass[french]{article}

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{empheq, stmaryrd}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\In}{in}
\DeclareMathOperator{\fst}{fst}
\DeclareMathOperator{\snd}{snd}
\DeclarePairedDelimiter\innerp\langle\rangle
\newcommand\sfF{\mathsf{F}}

\begin{document}

\begin{empheq}[left = {\empheqlbrack}]{alignat* = 2}
&{} \triangleright{} & \enspace &f \circ\In = \varphi\circ\sfF\innerp{f, \id}\\[-2ex]
\cline{2-4}\noalign{\vskip-0.5ex}
& & & f \\
& = & &\quad\text{-- pairing --} \\
& & & \fst\circ \innerp{f, \id} \\
& = & &\quad\text{-- cata-\textsc{Charn} --} \\
& \hphantom{{}={}} & &\hskip 0.75em \left[%
\begin{alignedat}{2}
& & & \innerp{f, \id}\circ \In \\
& & & \innerp{f\circ\In, \In} \\
& = & & \quad\text{-- $\sfF$ functor --} \\
& & & \innerp{f\circ\In, \In\circ\sfF\id} \\
& = & & \quad\text{-- pairing --} \\
& & & \innerp[\big]{f\circ\In, \In\circ\sfF(\snd\circ\innerp{f, \id})} \\
& = & & \quad\text{-- $\triangleleft, \mathsf{F}$ functor --} \\
& & & \innerp[\big]{\varphi\circ\sfF\innerp{f, \id}, \In\circ\sfF\:\snd\circ\sfF\:\innerp{f, \id}} \\
& = & & \quad\text{-- pairing --} \\
& & & \innerp{\varphi, \In\circ\sfF\:\snd}\circ\sfF\:\innerp{f, \id}
\end{alignedat}\right. \\[1ex]
& & & \fst\circ\llparenthesis\innerp{\varphi, \In\circ\sfF\snd}\rrparenthesis
\end{empheq}

\end{document}