Grammar: \[ M ::= x \mid \Pi x : M . M \mid \lambda x : M . M \mid M \, M \]
\(\beta\)-reduction: \[ (\lambda x : A . M) \, N \triangleright_\beta M [x / N] \]
Restatement: \[ \frac{}{\Gamma, x : A \vdash x : A} \]
Product formation: \[ \frac{\Gamma, x : A \vdash B : C}{\Gamma \vdash (\Pi x : A . B) : C} \]
Product introduction (a.k.a. abstraction): \[ \frac{\Gamma, x : A \vdash M : B}{\Gamma \vdash (\lambda x : A . M) : (\Pi x : A . B)} \]
Product elimination (a.k.a. application): \[ \frac{\Gamma \vdash M : (\Pi x : A . B) \qquad \Gamma \vdash N : A}{\Gamma \vdash M \, N : B [x / N]} \]
Conversion: \[ \frac{\Gamma \vdash M : A \qquad A =_\beta B}{\Gamma \vdash M : B} \]
Implication: \[ A \Rightarrow B = \forall x : A . B \] if \(x\) not free in \(B\).
Conjunction: \[ A \land B = \forall C : \prop . (A \Rightarrow B \Rightarrow C) \Rightarrow C \]
Disjunction: \[ A \lor B = \forall C : \prop . (A \Rightarrow C) \Rightarrow (B \Rightarrow C) \Rightarrow C \]
Negation: \[ \neg A = \forall C : \prop . A \Rightarrow C \]
Existential quantification: \[ \exists x : A . B = \forall C : \prop . (\forall x : A . B \Rightarrow C) \Rightarrow C \]