HOL Light

 ${\cfrac {\qquad }{\vdash t=t}}$ REFL reflexivity of equality ${\cfrac {\Gamma \vdash s=t\qquad \Delta \vdash t=u}{\Gamma \cup \Delta \vdash s=u}}$ TRANS transitivity of equality ${\cfrac {\Gamma \vdash f=g\qquad \Delta \vdash x=y}{\Gamma \cup \Delta \vdash f(x)=g(y)}}$ MK_COMB congruence of equality ${\cfrac {\Gamma \vdash s=t}{\Gamma \vdash (\lambda x.s)=(\lambda x.t)}}$ ABS abstraction of equality ($x$ must not be free in $\Gamma$ ) ${\cfrac {\qquad }{\vdash (\lambda x.t)x=t}}$ BETA connection of abstraction and function application ${\cfrac {\qquad }{\{p\}\vdash p}}$ ASSUME assuming $p$ , prove $p$ ${\cfrac {\Gamma \vdash p=q\qquad \Delta \vdash p}{\Gamma \cup \Delta \vdash q}}$ EQ_MP relation of equality and deduction ${\cfrac {\Gamma \vdash p\qquad \Delta \vdash q}{(\Gamma -\{q\})\cup (\Delta -\{p\})\vdash p=q}}$ DEDUCT_ANTISYM_RULE deduce equality from 2-way deducibility ${\cfrac {\Gamma [x_{1},\ldots ,x_{n}]\vdash p[x_{1},\ldots ,x_{n}]}{\Gamma [t_{1},\ldots ,t_{n}]\vdash p[t_{1},\ldots ,t_{n}]}}$ INST instantiate variables in assumptions and conclusion of theorem ${\cfrac {\Gamma [\alpha _{1},\ldots ,\alpha _{n}]\vdash p[\alpha _{1},\ldots ,\alpha _{n}]}{\Gamma [\tau _{1},\ldots ,\tau _{n}]\vdash p[\tau _{1},\ldots ,\tau _{n}]}}$ INST_TYPE instantiate type variables in assumptions and conclusion of theorem