Braces are mandatory, and each branch is a block. An if without else has an empty block as second branch.

\dfrac{\begin{array}{c} \Gamma \vdash e : \mathsf{bool} \qquad \Gamma \vdash \{c_1\} \dashv \Gamma \\ \Gamma \vdash \{c_2\} \dashv \Gamma \end{array}}{\Gamma \vdash \mathtt{if}\ (e)\ \{c_1\}\ \mathtt{else}\ \{c_2\} \dashv \Gamma}\;\textsf{(T-If)}

\dfrac{\rho, \sigma \vdash e \Rightarrow \mathsf{bool}\,\mathtt{true}, \sigma_1 \qquad \rho, \sigma_1 \vdash \{c_1\} \Rightarrow r, \rho, \sigma_2}{\rho, \sigma \vdash \mathtt{if}\ (e)\ \{c_1\}\ \mathtt{else}\ \{c_2\} \Rightarrow r, \rho, \sigma_2}\;\textsf{(If-T)}

\dfrac{\rho, \sigma \vdash e \Rightarrow \mathsf{bool}\,\mathtt{false}, \sigma_1 \qquad \rho, \sigma_1 \vdash \{c_2\} \Rightarrow r, \rho, \sigma_2}{\rho, \sigma \vdash \mathtt{if}\ (e)\ \{c_1\}\ \mathtt{else}\ \{c_2\} \Rightarrow r, \rho, \sigma_2}\;\textsf{(If-F)}

The implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.