Normal text with italics, bold, inline code and a link.

Inline math: \(\Gamma \vdash e : \tau\). Displayed math:

\[ \frac{\{P\}\ c_1\ \{Q\} \qquad \{Q\}\ c_2\ \{R\}}{\{P\}\ c_1; c_2\ \{R\}} \]

Lemma app_nil_r : forall (A : Type) (l : list A), l ++ [] = l.
Proof.
  induction l; simpl; auto.
  now rewrite IHl.
Qed.