diff --git a/prover/build b/prover/build
index 58551a797..34e6ec78f 100755
--- a/prover/build
+++ b/prover/build
@@ -18,9 +18,11 @@ proj = KProject()
 # Matching Logic Prover
 # =====================
 
-other_md_files = [ 'lang/smt-lang.md'
+other_md_files = [ 'lang/coq-lang.md'
+                 , 'lang/smt-lang.md'
                  , 'lang/kore-lang.md'
                  , 'drivers/base.md'
+                 , 'drivers/coq-driver.md'
                  , 'drivers/smt-driver.md'
                  , 'drivers/kore-driver.md'
                  , 'strategies/apply-equation.md'
@@ -34,6 +36,7 @@ other_md_files = [ 'lang/smt-lang.md'
                  , 'strategies/replace-evar-with-func-constant.md'
                  , 'strategies/simplification.md'
                  , 'strategies/search-bound.md'
+                 , 'strategies/typecheck.md'
                  , 'strategies/smt.md'
                  , 'strategies/unfolding.md'
                  , 'utils/load-named.md'
@@ -53,6 +56,7 @@ def prover(alias, flags = None):
 
 prover_kore = prover('prover-kore', '--main-module DRIVER-KORE --syntax-module DRIVER-KORE-SYNTAX')
 prover_smt  = prover('prover-smt',  '--main-module DRIVER-SMT  --syntax-module DRIVER-SMT-SYNTAX' )
+prover_coq  = prover('prover-coq',  '--main-module DRIVER-COQ  --syntax-module DRIVER-COQ-SYNTAX' )
 
 # Functional tests
 # ----------------
@@ -60,6 +64,8 @@ prover_smt  = prover('prover-smt',  '--main-module DRIVER-SMT  --syntax-module D
 # prover_kore.tests(inputs = glob('t/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine')
 # prover_smt .tests(inputs = glob('t/*.smt2'), flags = '-cCOMMANDLINE=.CommandLine')
 
+prover_coq .tests(inputs = glob('t/coq-tests/*.v'), flags = '-cCOMMANDLINE=.CommandLine')
+
 def log_on_success(file, message):
     return proj.rule( 'log-to-success'
                     , description = '$out: $message'
diff --git a/prover/coq_rules/coq_rules.pdf b/prover/coq_rules/coq_rules.pdf
new file mode 100644
index 000000000..28d4b684f
Binary files /dev/null and b/prover/coq_rules/coq_rules.pdf differ
diff --git a/prover/coq_rules/coq_rules.tex b/prover/coq_rules/coq_rules.tex
new file mode 100644
index 000000000..e214d8a6c
--- /dev/null
+++ b/prover/coq_rules/coq_rules.tex
@@ -0,0 +1,528 @@
+\documentclass{article}
+
+\usepackage{amsmath,amssymb,amsthm}
+\usepackage{fullpage}
+\usepackage{hyperref}
+\usepackage{longtable}
+\usepackage{mathtools}
+\usepackage{prftree}
+\usepackage[dvipsnames]{xcolor}
+\usepackage{xspace}
+
+\input{newcommands}
+
+\title{All Coq Rules in One Place}
+\author{Xiaohong Chen \and Lucas Pe{\~{n}}a}
+
+\begin{document}
+
+\maketitle
+
+\begin{abstract}
+This document summarizes all the proof rules of the Coq proof assistant,
+as listed in 
+\url{https://coq.inria.fr/distrib/current/refman/language/cic.html}.
+\end{abstract}
+
+\section{Syntax}
+
+Let us fix a countably infinite set $\V$ of \emph{variables}, denoted 
+$x,y,\dots$. 
+Let us fix a countably infinite set $\C$ of \emph{constants}, denoted
+$c,d,\dots$.
+
+\begin{definition}
+We define the set \CoqTerm to be the smallest set that satisfies the following 
+conditions:
+\begin{enumerate}
+\item $\SProp,\Prop,\Set \in \CoqTerm$; $\Type(i) \in \CoqTerm$ for every $i 
+\in \NNp$. 
+\item $\V \subseteq \CoqTerm$.
+\item $\C \subseteq \CoqTerm$.
+\item If $x \in \V$ and $T,U \in \CoqTerm$, 
+      then $\cfa{x}{T}{U} \in \CoqTerm$.
+\item If $x \in \V$ and $T,u \in \CoqTerm$,
+      then $\clm{x}{T}{u} \in \CoqTerm$.
+\item If $t,u \in \CoqTerm$,
+      then $\cpp{t}{u} \in \CoqTerm$, called \emph{application}.
+\item If $x \in \V$ and $t,T,u \in \CoqTerm$,
+      then $\clt{x}{t}{T}{u} \in \CoqTerm$.
+\end{enumerate}
+where $\cfa{x}{T}{U}$ binds $x$ to $U$
+and $\clm{x}{T}{u}$ binds $x$ to $u$.
+We use $\FV(T) \subseteq \V$ to denote the set of free variables in $T \in 
+\CoqTerm$. 
+For $T,U \in \CoqTerm$ and $x \in \V$, 
+we use $\sbs{T}{U}{x}$ to denote the result of substituting $U$ for $x$ in $T$,
+where $\alpha$-renaming happens implicitly to prevent variable capture.
+\end{definition}
+
+\begin{definition}
+We define the set 
+$\CoqSort = \{\SProp,\Prop,\Set\} \cup \{\Type(i) \mid i \in \NN\}$.
+Note that $\CoqSort \subseteq \CoqTerm$. 
+Elements in $\CoqSort$ are called \emph{sorts} and denoted as $s$,
+possibly with subscripts.
+\end{definition}
+
+\begin{definition}
+A \emph{local assumption} is written $\lasm{x}{T}$, where $x \in \V$ and $T \in 
+\CoqTerm$. 
+A \emph{local definition} is written $\ldef{x}{u}{T}$,
+where $x \in \V$ and $u,T \in \CoqTerm$.
+In both cases, we call $x$ the \emph{declared variable}. 
+A \emph{local context} is an ordered list of local assumptions and local 
+definitions, such that the declared variables are all distinct. 
+We use $\Gamma$, possibly with subscripts, to denote local contexts. 
+\end{definition}
+
+\begin{notation}\label{not:ldcl}
+We use the notation $[\lasm{x}{T} \scln \ldef{y}{u}{U} \scln \lasm{z}{V}]$
+to denote the local context that consists of
+the local assumption $\lasm{x}{T}$,
+the local definition $\ldef{y}{u}{U}$
+and the local assumption $\lasm{z}{V}$,
+with the implicit requirement that $x,y,z$ are all distinct.
+The empty local context is written as $[]$. 
+Let $\Gamma$ be a local context. 
+We write $x \in \Gamma$ to mean that $x$ is declared in $\Gamma$.
+We write $(\lasm{x}{T}) \in \Gamma$ to mean that the local assumption
+$\lasm{x}{T}$ is in $\Gamma$, or that
+the local definition $\ldef{x}{u}{T}$ is in $\Gamma$ for some $u \in \CoqTerm$.
+We write $(\ldef{x}{u}{T}) \in \Gamma$ to mean that
+the local definition $\ldef{x}{u}{T}$ is in $\Gamma$.
+We write $\Gamma \dcln ( \lasm{x}{T} )$ to denote the local context
+that enriches $\Gamma$ with $\lasm{x}{T}$, with the implicit requirement that 
+$x \not\in \Gamma$.
+Similarly, we write 
+$\Gamma \dcln ( \ldef{x}{u}{T} )$ to denote the local context
+that enriches $\Gamma$ with $\ldef{x}{u}{T}$, with the implicit requirement 
+that $x \not\in \Gamma$.
+We write $\Gamma_1 \scln \Gamma_2$ to mean the local context
+obtained by concatenating $\Gamma_1$ and $\Gamma_2$, with the implicit 
+requirement that all variables declared in $\Gamma_2$ are not declared in 
+$\Gamma_1$. 
+\end{notation}
+
+\begin{definition}
+A \emph{global assumption} is written $(\gasm{c}{T})$,
+with the parentheses, where $c \in \C$ and $T \in 
+\CoqTerm$. 
+A \emph{global definition} is written $\gldef{c}{u}{T}$,
+where $c \in \C$ and $u,T \in \CoqTerm$.
+In both cases, we call $c$ the \emph{declared constant}. 
+A \emph{global environment} is an ordered list of global assumptions and global
+definitions, and also \emph{declarations of inductive objects}, which are 
+defined later. 
+We use $E$, possibly with subscripts, to denote global environments.
+\end{definition}
+
+\begin{notation}
+We use the notation $\gasm{c_1}{T} \scln \gldef{c_2}{u}{U} \scln \gasm{c_3}{V}$
+to denote the local context that consists of
+the global assumption $\gasm{c_1}{T}$,
+the global definition $\gldef{c_2}{u}{U}$
+and the global assumption $\gasm{c_3}{V}$.
+The empty global context is written as $[]$. % TODO: is this right?
+Let $E$ be a local context. 
+We write $c \in E$ to mean that $c$ is declared in $E$.
+We write $(\gasm{c}{T}) \in E$ to mean that the global assumption
+$\gasm{c}{T}$ is in $E$, or that
+the global definition $\gldef{c}{u}{T}$ is in $E$ for some $u \in \CoqTerm$.
+We write $(\gldef{c}{u}{T}) \in E$ to mean that
+the global definition $\gldef{c}{u}{T}$ is in $E$.
+We write $E \scln \gasm{c}{T}$ to denote the global context
+that enriches $E$ with $\gasm{c}{T}$.
+Similarly, we write 
+$E \scln \gldef{c}{u}{T}$ to denote the global context
+that enriches $E$ with $( \gldef{c}{u}{T} )$.
+\end{notation}
+
+\begin{notation}
+We write $E[\Gamma] \proves \lasm{u}{T}$ to mean that $u$ is \emph{well-typed} 
+with type $T$ in global environment $E$ and local environment $\Gamma$.
+We write $\wf(E)[\Gamma]$ to mean that the global environment $E$ is 
+\emph{well-formed}
+and $\Gamma$ is a \emph{valid local context} in $E$.
+\end{notation}
+
+\begin{definition}
+A term $u$ is \emph{well-typed} in a global environment $E$ if there is a
+local context $\Gamma$ and type $T$ such that
+$E[\Gamma] \proves \lasm{u}{T}$ is derivable with the rules below.
+\end{definition}
+
+\section{Coq Rules}
+
+In this section we list all Coq rules. 
+A \emph{rule} consists of a set of \emph{premises} and one \emph{conclusion},
+separated by a horizontal bar.
+For readability, we put \emph{side conditions} alongside the premises.
+Side conditions are typed in $\sd{\text{green}}$, to distinguish
+from the premises.
+
+
+\subsection{Basic Typing Rules}
+
+There are 18 basic typing rules, as shown below. 
+
+
+\begin{center}
+\bgroup
+\def\arraystretch{4}
+\begin{longtable}{llp{5cm}}
+\textbf{Names} & \textbf{Rules} & \textbf{Comments} \\\hline
+\prule{W-Empty}&
+$\prftree{\cdot}{\wf([])[]}$ &
+The empty global environment is well-formed, and the empty local context is a 
+valid local context in the empty global environment.\\
+\prule{W-Local-Assum}&
+$\prftree{E[\Gamma]\vdash T \cln s}
+{\sd{s \in S}}
+{\sd{x \not\in \Gamma}}
+{\wf(E)[\Gamma \dcln (x \cln T)]}$&
+The side condition $x \not\in \Gamma$ needs not to be specified because 
+it is implicit
+in the notation $\Gamma \dcln (x \cln T)$; see Notation~\ref{not:ldcl}.\\
+\prule{W-Local-Def}&
+$\prftree{E[\Gamma]\vdash t \cln T}
+{\sd{x \not\in \Gamma}}
+{\wf(E)[\Gamma \dcln (\ldef{x}{t}{T})]}$&
+The side condition $x \not\in \Gamma$ needs not to be specified because 
+it is implicitly implied 
+by the notation $\Gamma \dcln (\ldef{x}{t}{T})$; see Notation~\ref{not:ldcl}.\\
+\prule{W-Global-Assum}&
+$
+\prftree
+{E[]\vdash T \cln s}
+{\sd{s \in S}}
+{\sd{c \not\in E}}
+{\wf(E ; c \cln T)[]}
+$ & \\
+\prule{W-Global-Def} &
+$
+\prftree
+{E[]\vdash t \cln T}
+{\sd{c \not\in E}}
+{\wf(E ; \gldef{c}{t}{T})[]}
+$ & \\
+\prule{Ax-SProp} &
+$
+\prftree{\wf(E)[\Gamma]}
+{E[\Gamma] \vdash \SProp \cln \Type(1)}
+$ &\\
+\prule{Ax-Prop} &
+$
+\prftree{\wf(E)[\Gamma]}
+{E[\Gamma] \vdash \Prop \cln \Type(1)}
+$ &\\
+\prule{Ax-Set} &
+$
+\prftree{\wf(E)[\Gamma]}
+{E[\Gamma] \vdash \Set \cln \Type(1)}
+$ &\\
+\prule{Ax-Type} &
+$
+\prftree{\wf(E)[\Gamma]}
+{E[\Gamma] \vdash \Type(i) \cln \Type(i+1)}
+$ & Here, $i \in \NNp$ is any positive natural number. \\
+\prule{Var} &
+\multicolumn{2}{l}{
+$
+\prftree{\wf(E)[\Gamma]}
+{\sd{\text{$(\lasm{x}{T} \in \Gamma)$, or $(\ldef{x}{t}{T}) \in \Gamma$ for 
+some $t \in \CoqTerm$}}}
+{E[\Gamma] \vdash x \cln T}
+$} \\
+\prule{Const} &
+\multicolumn{2}{l}{
+$
+\prftree{\wf(E)[\Gamma]}
+{\sd{\text{$(\lasm{c}{T} \in E)$, or $(\ldef{c}{t}{T}) \in E$ for 
+some $t \in \CoqTerm$}}}
+{E[\Gamma] \vdash c \cln T}
+$} \\
+\prule{Prod-SProp} &
+$
+\prftree
+{E[\Gamma] \vdash T \cln s}
+{\sd{s \in S}}
+{E[\Gamma \dcln (x \cln T)] \vdash U \cln \SProp}
+{E[\Gamma]\vdash \cfa{x}{T}{U} \cln \SProp}
+$ &\\
+\prule{Prod-Prop} &
+$
+\prftree
+{E[\Gamma] \vdash T \cln s}
+{\sd{s \in S}}
+{E[\Gamma \dcln (x \cln T)] \vdash U \cln \Prop}
+{E[\Gamma]\vdash \cfa{x}{T}{U} \cln \Prop}
+$ &\\
+\prule{Prod-Set} &
+\multicolumn{2}{l}{
+$
+\prftree
+{E[\Gamma] \vdash T \cln s}
+{\sd{s \in \{\SProp,\Prop,\Set\}}}
+{E[\Gamma \dcln (x \cln T)] \vdash U \cln \Set}
+{E[\Gamma]\vdash \cfa{x}{T}{U} \cln \Set}
+$
+} \\
+\prule{Prod-Type} &
+\multicolumn{2}{l}{
+$
+\prftree
+{E[\Gamma] \vdash T \cln s}
+{\sd{s \in \{\SProp,\Type(i)\}}}
+{E[\Gamma \dcln (x \cln T)] \vdash U \cln \Type(i)}
+{E[\Gamma]\vdash \cfa{x}{T}{U} \cln \Type(i)}
+$
+} \\
+\prule{Lam} &
+$
+\prftree
+{E[\Gamma] \vdash \cfa{x}{T}{U} \cln s}
+{\sd{s \in S}}
+{E[\Gamma \dcln (x \cln T)] \vdash t \cln U}
+{E[\Gamma] \vdash \clm{x}{T}{t} \cln \cfa{x}{T}{U}}
+$ &\\
+\prule{App} &
+$
+\prftree
+{E[\Gamma] \vdash t \cln \cfa{x}{U}{T}}
+{E[\Gamma] \vdash u \cln U}
+{E[\Gamma] \vdash (t \, u) \cln T[u/x]}
+$ &\\
+\prule{Let} &
+$\prftree
+{E[\Gamma] \vdash t \cln T}
+{E[\Gamma \dcln (\ldef{x}{t}{T})] \vdash u \cln U}
+{E[\Gamma] \vdash \clt{x}{t}{T}{u} \cln U[t/x]}
+$
+\end{longtable}
+\egroup
+\end{center}
+
+\subsection{Conversion Rules}
+In this section, we define what it means for two Coq programs to be
+\emph{intentionally equal}, or \emph{convertible}.
+
+\begin{center}
+\bgroup
+\def\arraystretch{4}
+\begin{longtable}{llp{5cm}}
+\textbf{Names} & \textbf{Rules} & \textbf{Comments} \\\hline
+\prule{Beta}&
+$\prftree{E[\Gamma] \vdash ((\clm{x}{T}{t}) u) \red_{\beta} \sbs{t}{x}{u}}$&
+We say that $\sbs{t}{x}{u}$ is the \emph{$\beta$-contraction} of
+$((\clm{x}{T}{t}) u)$, and that $((\clm{x}{T}{t}) u)$ is the
+\emph{$\beta$-expansion} of $\sbs{t}{x}{u}$ \\
+&&
+$\iota$-reduction rules to be defined later \\
+\prule{Delta-Local}&
+$\prftree
+{\wf(E)[\Gamma]}
+{(\ldef{x}{t}{T}) \in \Gamma}
+{E[\Gamma] \vdash x \red_{\Delta} t}$&
+Reducing variable defined in local context \\
+\prule{Delta-Local}&
+$\prftree
+{\wf(E)[\Gamma]}
+{(\gldef{c}{t}{T}) \in E}
+{E[\Gamma] \vdash c \red_{\delta} t}$&
+Reducing constant defined in global context \\
+\prule{Zeta}&
+$\prftree
+{\wf(E)[\Gamma]}
+{E[\Gamma] \vdash \lasm{u}{U}}
+{E[\Gamma \dcln (\ldef{x}{u}{U})] \vdash \lasm{t}{T}}
+{E[\Gamma] \vdash \clt{x}{u}{U}{t} \red_{\zeta} \sbs{t}{x}{x}}$&
+Remove local definitions occurring in terms \\
+\end{longtable}
+\egroup
+\end{center}
+In addition to the above convertibility rules, we also allow identifying a term
+$t$ of type $\cfa{x}{t}{U}$ with its \emph{$\eta$-expansion} $\clm{x}{T}{(t x)}$
+for $x$ fresh in $t$. Note \emph{$\eta$-reduction} is deliberately not defined.
+% TODO: show example?
+
+\begin{notation}
+We write $E[\Gamma] \vdash t \red u$ for the contextual closure of the rules
+defined above. That is, $t$ reduces to $u$ with global environment $E$ and local
+context $\Gamma$ with one of the previous reductions $\beta, \Delta, \delta,
+\iota,$ or $\zeta$.
+\end{notation}
+
+\begin{definition}
+Two terms are called \emph{irrelevant} if they share a common type of a strict
+proposition $\gasm{A}{\SProp}$. Irrelevant terms can be identified.
+\end{definition}
+
+\begin{definition}
+Two terms $t_1, t_2$ are called \emph{$\beta\delta\iota\zeta\eta$-convertible}, or
+\emph{convertible}, or \emph{equivalent} in global environment $E$ and local
+context $\Gamma$ iff there exists $t_1, t_2$ such that
+\[ E[\Gamma] \vdash t_1 \red \ldots \red u_1 \text{  and  } E[\Gamma] \vdash t_2 \red \ldots \red u_2  \]
+and either $u_1$ and $u_2$ are identical up irrelevant subterms, or they are
+convertible up to $\eta$-exxpansion. We denote this as
+$E[\Gamma] \vdash t_1 \conveq t_2$
+\end{definition}
+
+\subsection{Subtyping Rules}
+The \emph{subtyping} relation is inductively defined as follows:
+% TODO: display as proof rules?
+\begin{itemize}
+\item if $E[\Gamma] \vdash t \conveq u$, then $E[\Gamma] \vdash t \subty u$
+\item if $i \leq j$, then $E[\Gamma] \vdash \Type(i) \subty \Type(j)$
+\item $E[\Gamma] \vdash \Set \subty \Type(i)$ for all $i$
+\item $E[\Gamma] \vdash \Prop \subty \Set$
+\item if $E[\Gamma] \vdash T \conveq U$ and
+  $E[\Gamma \dcln (\lasm{x}{T})] \vdash T' \subty U'$, then
+  $E[\Gamma] \vdash \cfa{x}{T}{T'} \subty \cfa{x}{U}{U'}$
+\end{itemize}
+
+\subsection{Conversion/Subtyping: Polymorphic Universes}
+
+\subsection{Conversion Typing Rule}
+We now have the infrastructure to define the typing rule for conversion:
+\[
+\prule{Conv}\hspace{5ex}
+\prftree
+{E[\Gamma] \vdash \lasm{U}{s}}
+{E[\Gamma] \vdash \lasm{t}{T}}
+{E[\Gamma] T \subty U}
+{E[\Gamma] \vdash \lasm{t}{U}}
+\]
+
+\subsection{Inductive Definitions}
+\begin{definition}
+We represent an \emph{inductive definition} as $\Ind{p}{\Gamma_I}{\Gamma_C}$ where
+\begin{itemize}
+\item $p$ represents the number of parameters of the inductive types
+\item $\Gamma_I$ represents the names and types of inductive types
+\item $\Gamma_C$ represents the names and types of the constructors of the inductive types
+\end{itemize}
+\end{definition}
+
+\begin{definition}
+Let $\Ind{p}{\Gamma_I}{\Gamma_C}$ be an inductive definition and let $T$ be such
+that $(t \cln T) \in \Gamma_I \cup \Gamma_C$. Then, there exists a
+$\Gamma_P = [a_1 \cln A_1 \scln \ldots \scln a_p \cln A_p]$ such that $T$ can be
+written as $\forall \Gamma_P, T'$ for some $T'$. Here $\Gamma_P$ is called the
+\emph{context of paramters}.
+
+Additionaly, if $(t \cln T) \in \Gamma_I$, then $T$ can be written as
+$\forall \Gamma_P, \Gamma_{\mathit{Arr}(t)}, s$. Here, $\mathit{Arr}(t)$ is
+called the \emph{Arity} of the inductive type $t$ and $s$ is called the sort of
+$t$.
+\end{definition}
+
+\begin{example}
+The inductive definition for parameterized lists is:
+\[
+\Ind{1}{\begin{bmatrix} \mathsf{list} \cln \Set \rightarrow \Set \end{bmatrix}}
+    {\begin{bmatrix*}[l]
+        \mathsf{nil}\, &: \,\forall A \cln \Set,\, \mathsf{list}\, A \\
+        \mathsf{cons}\, &: \, \forall A \cln \Set,\, A\, \rightarrow\, \mathsf{list}\, A\,
+          \rightarrow\, \mathsf{list}\, A
+    \end{bmatrix*}}
+\]
+This corresponds to the Coq definition:
+\begin{verbatim}
+Inductive list (A:Set) : Set :=
+| nil : list A
+| cons : A -> list A -> list A.
+\end{verbatim}
+\end{example}
+
+Below are rules for types of constants in a global environment that contain an
+inductive definition:
+\[
+\prule{Ind}\hspace{5ex}
+\prftree
+{\wf(E)[\Gamma]}
+{\Ind{p}{\Gamma_I}{\Gamma_C} \in E}
+{\lasm{a}{A} \in \Gamma_I}
+{E[\Gamma] \vdash \lasm{a}{A}}
+\]
+\[
+\prule{Constr}\hspace{5ex}
+\prftree
+{\wf(E)[\Gamma]}
+{\Ind{p}{\Gamma_I}{\Gamma_C} \in E}
+{\lasm{c}{C} \in \Gamma_C}
+{E[\Gamma] \vdash \lasm{c}{C}}
+\]
+
+\begin{definition}
+A type $T$ is an \emph{arity of sort $s$} if it converts to the sort $s$ or to a
+product $\cfa{x}{T}{U}$ with $U$ an arity of sort $s$.
+\end{definition}
+\begin{definition}
+A type $T$ is an \emph{arity} if there is an $s \in S$ such that $T$ is an arity
+of sort $s$.
+\end{definition}
+
+\begin{definition}
+A type $T$ is a \emph{type of constructor of $I$} if $T$ is $(I\, t_1 \ldots t_n)$ or
+$T$ is $\cfa{x}{U}{T'}$ where $T'$ is a type of constructor of $I$.
+\end{definition}
+
+\begin{definition}
+A type of constructor $T$ is said to \emph{satisfy the positivity condition} for
+$X$ if $T = (X\, t_1 \ldots t_n)$ and $X$ does not occur free in any $t_i$, or
+$T = \cfa{x}{U}{V}$ where $X$ occurs only strictly positively in $U$ and
+$V$ satisfies the positivity condition for $X$.
+\end{definition}
+\begin{definition}
+A constant $X$ occurs \emph{strictly positive} in $T$ if one of the following
+cases hold:
+\begin{itemize}
+\item $X$ does not occur in $T$
+\item $T$ converts to $(X\, t_1 \ldots t_n)$ and $X$ does not occur in any $T_i$
+\item $T$ converts to $\cfa{x}{U}{V}$ where $X$ does not occur in $U$ and
+  $X$ occurs strictly positively in $V$
+\item $T$ converts to $(I\, a_1\ldots a_m\, t_1\ldots t_p)$ where $I$ represents
+  the inductive definition
+  \[\Ind{m}{\lasm{I}{A}}{\lasm{c_1}{\forall p_1 \cln P_1, \ldots \forall p_m \cln P_m, C_1}
+    \scln \ldots \lasm{c_n}{\forall p_1 \cln P_1, \ldots \forall p_m \cln P_m, C_n}}
+  \]
+  and $X$ does not occur in any of the $t_i$, and all instantiated types of
+  constructors $C_i\{p_j/a_j\}_{j=1\ldots m}$ satisfy the nested positivity
+  condition for $X$
+\end{itemize}
+\end{definition}
+\begin{definition}
+A type of constructor $T$ of $I$ is said to \emph{satisfy the nested positivity
+  condition} for $X$ if $T = (I\, b_1 \ldots b_n u_1 \ldots u_p)$ where $I$ is
+an inductive type with $m$ paramters and $X$ does not occur in any $u_i$, or
+$T = \cfa{x}{U}{V}$ where $X$ occurs only strictly positively in $U$ and $V$
+satisfies the nested positivity condition for $X$.
+\end{definition}
+
+\subsubsection{Correctness Rules}
+Let $E$ be a global environment and $\Gamma_P, \Gamma_I, \Gamma_C$ be contexts
+such that $\Gamma_I$ is
+$[I_1\cln \forall\Gamma_P, A_1 \scln \ldots I_k\cln \forall \Gamma_P, A_k]$
+and $\Gamma_C$ is
+$[c_1\cln \forall\Gamma_P, C_1 \scln \ldots c_n\cln \forall \Gamma_P, C_n]$.
+Then we have the following well-formedness rule:
+\[
+\prule{Ind}\hspace{5ex}
+\prftree
+{\wf(E)[\Gamma_P]}
+{(E[\Gamma_I\scln\Gamma_P] \vdash \lasm{C_i}{s_{q_i}})_i=1\ldots n}
+{\wf(E\scln \Ind{p}{\Gamma_I}{\Gamma_C})[]}
+\]
+provided the following side conditions hold:
+\begin{itemize}
+\item $k > 0$ and all $I_j$ and $c_i$ are distinct names for $j=1\ldots k$ and
+  $i=1\ldots n$
+\item $p$ is the number of parameters of $\Ind{p}{\Gamma_I}{\Gamma_C}$ and
+  $\Gamma_P$ is the context of paramters
+\item for $j=1\ldots k$, $A_j$ is an arity of sort $s_j$ and $I_j \not\in E$
+\item for $i=1\ldots n$, $C_i$ is a type of constructor of $I_{q_i}$ which
+  satisfies the positivity condition for $I_1 \ldots I_k$ and $c_i \not\in E$
+\end{itemize}
+
+\end{document}
diff --git a/prover/coq_rules/newcommands.tex b/prover/coq_rules/newcommands.tex
new file mode 100644
index 000000000..b40e2d2e3
--- /dev/null
+++ b/prover/coq_rules/newcommands.tex
@@ -0,0 +1,42 @@
+\theoremstyle{definition}
+\newtheorem{definition}{Definition}[section]
+\newtheorem{notation}[definition]{Notation}
+\newtheorem{example}[definition]{Example}
+
+\newcommand{\CoqTerm}{\textnormal{\textit{Term}}\xspace}
+\newcommand{\CoqSort}{\textnormal{\textit{Sort}}\xspace}
+
+\newcommand{\SProp}{\mathsf{SProp}}
+\newcommand{\Prop}{\mathsf{Prop}}
+\newcommand{\Set}{\mathsf{Set}}
+\newcommand{\Type}{\mathsf{Type}}
+\newcommand{\NN}{\mathbb{N}}
+\newcommand{\NNp}{{\NN_{\ge 1}}}
+\newcommand{\V}{V}
+\newcommand{\C}{C}
+\newcommand{\cln}{{\,:\,}}
+\newcommand{\scln}{\mathbin{;}}
+\newcommand{\dcln}{\mathbin{::}}
+\newcommand{\FV}{\mathrm{FV}}
+\newcommand{\sbs}[3]{#1 [ #2 / #3 ]}
+
+\newcommand{\cfa}[3]{\forall #1 \cln #2 , #3}
+\newcommand{\clm}[3]{\lambda #1 \cln #2 . #3}
+\newcommand{\cpp}[2]{(#1 \, #2)}
+\newcommand{\clt}[4]{\textsf{let} \, #1 \coloneqq #2 \cln #3 \,\textsf{in}\, #4}
+
+\newcommand{\lasm}[2]{#1 \cln #2}
+\newcommand{\gasm}[2]{#1 \cln #2}
+\newcommand{\ldef}[3]{#1 \coloneqq #2 \cln #3}
+\newcommand{\gldef}[3]{#1 \coloneqq #2 \cln #3}
+
+\newcommand{\proves}{\vdash}
+\newcommand{\wf}{\mathcal{W\!F}}
+\newcommand{\prule}[1]{\textsc{(#1)}}
+\newcommand{\sd}[1]{{{\color{JungleGreen} #1}}}
+
+\newcommand{\red}{\triangleright}
+\newcommand{\conveq}{=_{\beta\delta\iota\zeta\eta}}
+\newcommand{\subty}{\leq_{\beta\delta\iota\zeta\eta}}
+
+\newcommand{\Ind}[3]{\mathsf{Ind}[#1]\left(#2 \coloneqq #3\right)}
diff --git a/prover/drivers/base.md b/prover/drivers/base.md
index 9ec7a5afb..d13fa8c8c 100644
--- a/prover/drivers/base.md
+++ b/prover/drivers/base.md
@@ -79,6 +79,7 @@ module DRIVER-BASE
   imports STRATEGY-UNFOLDING
   imports STRATEGY-KNASTER-TARSKI
   imports STRATEGY-REPLACE-EVAR-WITH-FUNC-CONSTANT
+  imports STRATEGY-TYPECHECK
   imports SYNTACTIC-MATCH-RULES
   imports VISITOR
   imports PATTERN-LENGTH
diff --git a/prover/drivers/coq-driver.md b/prover/drivers/coq-driver.md
new file mode 100644
index 000000000..06fe7b0bb
--- /dev/null
+++ b/prover/drivers/coq-driver.md
@@ -0,0 +1,168 @@
+Coq Driver
+==========
+
+This file is responsible for loading definitions in the Coq format.
+
+```k
+module DRIVER-COQ-COMMON
+  imports COQ
+  imports STRATEGIES-EXPORTED-SYNTAX
+  syntax Pgm ::= CoqSentences
+endmodule
+```
+
+```k
+module DRIVER-COQ-SYNTAX
+  imports DRIVER-BASE-SYNTAX
+  imports DRIVER-COQ-COMMON
+  imports COQ-SYNTAX
+endmodule
+```
+
+```k
+module DRIVER-COQ
+  imports DRIVER-KORE
+  imports DRIVER-COQ-COMMON
+  imports KORE
+  imports PROVER-CONFIGURATION
+  imports PROVER-CORE-SYNTAX
+  imports STRATEGIES-EXPORTED-SYNTAX
+
+// Add sort "Term" to declarations
+  rule <k> CS:CoqSentence CSs:CoqSentences => CS ~> CSs ... </k>
+       <declarations> ( .Bag
+                     => <declaration> sort #token("Term", "UpperName") </declaration>
+                      ) ...
+       </declarations>
+
+// Add symbol (of sort Term) and equality axiom corresponding to each definition
+  rule <k> Definition ID : TYPE := TERM .
+        => .K
+           ...
+       </k>
+       <declarations> ( .Bag
+                     => <declaration> symbol CoqIdentToSymbol(ID)(.Sorts) : #token("Term", "UpperName") </declaration>
+                        <declaration> axiom getFreshGlobalAxiomName() : \equals(CoqIdentToSymbol(ID), CoqTermToPattern(TERM)) </declaration>
+                      ) ...
+       </declarations>
+       <goals>
+         ( .Bag =>
+           <goal>
+             <id> !N:ClaimName </id>
+             <active> true:Bool </active>
+             <parent> .K </parent>
+             <claim> \type(CoqIdentToSymbol(ID), CoqTermToPattern(TYPE)) </claim>
+             <strategy> typecheck </strategy>
+             <expected> success </expected>
+             <local-context> .Bag </local-context>
+             <trace> .K </trace>
+           </goal>
+         )
+         ...
+       </goals>
+
+
+// Translate inductive cases
+  rule <k> Inductive ID BINDERs : TERM := .CoqIndCases .
+        => .K
+           ...
+       </k>
+       <declarations> ( .Bag
+                     => <declaration> symbol CoqIdentToSymbol(ID)(.Sorts) : #token("Term", "UpperName") </declaration>
+                      ) ...
+       </declarations>
+
+  rule <k> Inductive ID BINDERs : TERM := (IDC BINDERCs : TERMC) | CASEs .
+        => Inductive ID BINDERs : TERM := CASEs .
+           ...
+       </k>
+       <declarations> ( .Bag
+                     => <declaration> symbol CoqIdentToSymbol(IDC)(.Sorts) : #token("Term", "UpperName") </declaration>
+                        <declaration> axiom getFreshGlobalAxiomName() : \type(CoqIdentToSymbol(IDC)(.Patterns), CoqTermToPattern(TERMC))  </declaration>
+                      ) ...
+       </declarations>
+
+// Converting Term to Pattern
+  syntax Pattern ::= CoqTermToPattern(CoqTerm) [function]
+  rule CoqTermToPattern(UN:UpperName) => CoqIdentToSymbol(UN)
+  rule CoqTermToPattern(LN:LowerName) => CoqIdentToSymbol(LN)
+  rule CoqTermToPattern(#token("Prop", "CoqSort")) => #token("Term", "UpperName")
+  rule CoqTermToPattern(fun BINDERs => TERM) => \lambda { CoqBindersToPatterns(BINDERs) } CoqTermToPattern(TERM)
+  rule CoqTermToPattern(forall BINDERs, TERM) => \pi { CoqBindersToPatterns(BINDERs) } CoqTermToPattern(TERM)
+  rule CoqTermToPattern(match Ts return P with EQs end) => CoqTermToPattern(match Ts with EQs end)
+  rule CoqTermToPattern(match Ts with .CoqEquations end) => \bottom()
+  rule CoqTermToPattern(match Ts with (| MP:CoqMultPattern => TM:CoqTerm) | EQs end)
+    => CoqTermToPattern(match Ts with (MP:CoqMultPattern => TM:CoqTerm) | EQs end)
+  rule CoqTermToPattern(match Ts with (MP:CoqMultPattern => TM:CoqTerm) | EQs end) =>
+       \or( #flattenOrs(
+         \or( \exists { CoqMultPatternToBinders(MP) }
+                \and( #equals(CoqMatchItemsToPatterns(Ts), CoqMultPatternToPatterns(MP))
+                    ++Patterns
+                    CoqTermToPattern(TM)
+                    )
+            ++Patterns
+            CoqTermToPattern(match Ts with EQs end)
+            ), .Patterns))
+  rule CoqTermToPattern(TM:CoqTerm ARG) => CoqTermToPattern(TM)(CoqArgToPatterns(ARG))
+  rule CoqTermToPattern(fix ID BINDERs ANN:CoqAnnotation : TY := TM) => CoqTermToPattern(fix ID BINDERs : TY := TM)
+  rule CoqTermToPattern(fix ID BINDERs : TY := TM) => \mu { # CoqNameToVariableName(ID) } CoqTermToPattern(fun BINDERs => TM)
+  rule CoqTermToPattern(@ QID:CoqQualID TM:CoqTerm) => CoqIdentToSymbol(QID)(CoqTermToPattern(TM))
+  // TODO: incorporate qualfied name
+  rule CoqTermToPattern(QID:CoqQualID . ID:CoqIdent) => CoqIdentToSymbol(ID)
+  // TODO: do we need to do anything with the type here?
+  rule CoqTermToPattern((TM:CoqTerm : TY:CoqTerm):CoqTerm) => CoqTermToPattern(TM)
+
+  syntax Patterns ::= CoqArgToPatterns(CoqArg) [function]
+  rule CoqArgToPatterns(ARG1 ARG2) => CoqArgToPatterns(ARG1) ++Patterns CoqArgToPatterns(ARG2)
+  rule CoqArgToPatterns(TM:CoqTerm) => CoqTermToPattern(TM), .Patterns
+   [owise]
+
+  syntax Patterns ::= CoqMatchItemsToPatterns(CoqMatchItems) [function]
+  syntax Pattern ::= CoqMatchItemToPattern(CoqMatchItem) [function]
+  rule CoqMatchItemsToPatterns(.CoqMatchItems) => .Patterns
+  rule CoqMatchItemsToPatterns(MI:CoqMatchItem, MIs) => CoqMatchItemToPattern(MI), .Patterns
+
+  rule CoqMatchItemToPattern(MI:CoqTerm) => CoqTermToPattern(MI)
+  // TODO: is this right?
+  rule CoqMatchItemToPattern(MI:CoqTerm as N:CoqName) => CoqTermToPattern(MI)
+
+  syntax Patterns ::= #equals(Patterns, Patterns) [function]
+  rule #equals(.Patterns, .Patterns) => .Patterns
+  rule #equals((P1, Ps1), (P2, Ps2)) => \equals(P1, P2), #equals(Ps1, Ps2)
+
+  syntax Pattern ::= CoqPatternToPattern(CoqPattern) [function]
+  syntax Patterns ::= CoqPatternToPatterns(CoqPattern) [function]
+  syntax Patterns ::= CoqMultPatternToPatterns(CoqMultPattern) [function]
+  rule CoqMultPatternToPatterns(.CoqMultPattern) => .Patterns
+  rule CoqMultPatternToPatterns(MP, MPs) => CoqPatternToPattern(MP), CoqMultPatternToPatterns(MPs)
+
+  rule CoqPatternToPattern(ID:CoqQualID) => CoqIdentToSymbol(ID)
+  syntax Symbol ::= #stuck() [function]
+  rule CoqPatternToPattern(ID:CoqQualID P:CoqPattern) => CoqIdentToSymbol(ID)(CoqPatternToPatterns(P))
+  rule CoqPatternToPatterns(ID:CoqQualID) => CoqIdentToSymbol(ID), .Patterns
+  rule CoqPatternToPatterns(ID:CoqQualID P:CoqPattern) => CoqIdentToSymbol(ID) ++Patterns CoqPatternToPatterns(P)
+  rule CoqPatternToPatterns(U:Underscore P:CoqPattern) => !S:Symbol ++Patterns CoqPatternToPatterns(P)
+
+// Get binders from MultPattern
+  syntax Patterns ::= CoqMultPatternToBinders(CoqMultPattern) [function]
+  syntax Patterns ::= CoqPatternToBinders(CoqMultPattern) [function]
+  rule CoqMultPatternToBinders(ID:CoqQualID) => .Patterns
+  rule CoqMultPatternToBinders(ID:CoqQualID P:CoqPattern) => CoqPatternToBinders(P)
+  rule CoqPatternToBinders(ID:CoqQualID) => CoqIdentToSymbol(ID), .Patterns
+  rule CoqPatternToBinders(ID:CoqQualID P:CoqPattern) => CoqIdentToSymbol(ID), CoqPatternToBinders(P)
+  rule CoqPatternToBinders(U:Underscore P:CoqPattern) => !S:Symbol, CoqPatternToBinders(P)
+
+  syntax Patterns ::= CoqBindersToPatterns(CoqBinders) [function]
+  rule CoqBindersToPatterns(.CoqBinders) => .Patterns
+  rule CoqBindersToPatterns(BINDER BINDERs:CoqBinders) =>
+       CoqBinderToPatterns(BINDER) ++Patterns CoqBindersToPatterns(BINDERs)
+
+  syntax Patterns ::= CoqBinderToPatterns(CoqBinder) [function]
+  rule CoqBinderToPatterns(NAME:CoqName) => CoqNameToVariableName(NAME) { #token("Term", "UpperName") }
+  rule CoqBinderToPatterns((.CoqNames : TYPE:CoqTerm)) => .Patterns
+  rule CoqBinderToPatterns(((NAME:CoqName NAMES:CoqNames) : TYPE:CoqTerm)) => CoqNameToVariableName(NAME) { #token("Term", "UpperName") }, CoqBinderToPatterns((NAMES : TYPE))
+```
+
+```k
+endmodule
+```
diff --git a/prover/ext/k b/prover/ext/k
index 0d2819ac8..8ebd956aa 160000
--- a/prover/ext/k
+++ b/prover/ext/k
@@ -1 +1 @@
-Subproject commit 0d2819ac873a6c9a448de4da3060b1ba1e682bb2
+Subproject commit 8ebd956aa1e344ed1d2e0ce15b22b251435839c3
diff --git a/prover/lang/coq-lang.md b/prover/lang/coq-lang.md
new file mode 100644
index 000000000..275688611
--- /dev/null
+++ b/prover/lang/coq-lang.md
@@ -0,0 +1,125 @@
+```k
+module COQ-SYNTAX
+  imports TOKENS-SYNTAX
+  imports COQ
+endmodule
+
+module COQ
+  imports INT-SYNTAX
+  imports BOOL-SYNTAX
+  imports STRING
+  imports KORE-HELPERS
+
+// Identifiers
+  syntax CoqIdent ::= LowerName
+                    | UpperName
+  syntax CoqQualID ::= CoqIdent
+                     | CoqQualID "." CoqIdent
+                     | Underscore
+  syntax CoqName ::= CoqIdent
+                   | Underscore
+  syntax CoqNames ::= List{CoqName, ""} [klabel(CoqNames)]
+
+// Sorts
+  syntax CoqSort ::= "SProp" [token]
+                   | "Prop"  [token]
+                   // | "Set"   [token]
+                   | "Type"  [token]
+
+// Seralize to String:
+  syntax String ::= CoqNameToString(CoqName) [function, functional, hook(STRING.token2string)]
+
+// Sort conversions
+  syntax Symbol ::= CoqIdentToSymbol(CoqIdent) [function]
+  rule CoqIdentToSymbol(IDENT:UpperName) => IDENT
+  rule CoqIdentToSymbol(IDENT:LowerName) => IDENT
+
+  syntax Symbol ::= CoqQualIDToSymbol(CoqQualID) [function]
+  rule CoqQualIDToSymbol(ID:CoqIdent) => CoqIdentToSymbol(ID)
+
+  syntax VariableName ::= CoqNameToVariableName(CoqName) [function]
+  rule CoqNameToVariableName(NAME) => StringToVariableName(CoqNameToString(NAME))
+
+  syntax Sorts ::= CoqNamesToSorts(CoqNames) [function]
+  rule CoqNamesToSorts(.CoqNames) => .Sorts
+  rule CoqNamesToSorts(NAME:CoqName NAMEs) => StringToSort("Term"), CoqNamesToSorts(NAMEs)
+
+// Terms
+  syntax CoqTerm ::= "fun" CoqBinders "=>" CoqTerm
+                   | "fix" CoqFixBodies
+                   | "cofix" CoqCofixBodies
+                   | "let" CoqIdent ":=" CoqTerm "in" CoqTerm
+                   | "let" CoqIdent CoqBinders ":" CoqTerm ":=" CoqTerm "in" CoqTerm
+                   | "@" CoqQualID CoqTerm
+                   | "match" CoqMatchItems "with" CoqEquations "end"
+                   | "match" CoqMatchItems CoqReturnType "with" CoqEquations "end"
+                   | CoqTerm ":" CoqTerm
+                   > CoqTerm CoqArg [right]
+                   | CoqQualID
+                   | CoqSort
+                   | Int
+                   | Underscore
+                   > "forall" CoqBinders "," CoqTerm
+                   > "(" CoqTerm ")" [bracket]
+
+  syntax CoqBinder ::= CoqName
+                     | "(" CoqNames ":" CoqTerm ")"
+  syntax CoqBinders ::= List{CoqBinder, ""} [klabel(CoqBinders)]
+
+  syntax CoqArg ::= CoqArg CoqArg
+                  | "(" CoqIdent ":=" CoqTerm ")"
+                  > CoqTerm
+  syntax CoqTerms ::= List{CoqTerm, ""} [klabel(CoqTerms)]
+
+  syntax CoqFixBody ::= CoqIdent CoqBinders ":" CoqTerm ":=" CoqTerm
+                      | CoqIdent CoqBinders CoqAnnotation ":" CoqTerm ":=" CoqTerm
+  syntax CoqFixBodyList ::= List{CoqFixBody, "with"}
+  syntax CoqFixBodies ::= CoqFixBody
+                        | CoqFixBody CoqFixBodyList "for" CoqIdent
+  syntax CoqAnnotation ::= "{" "struct" CoqIdent "}"
+
+  syntax CoqCofixBody ::= CoqIdent CoqBinders ":" CoqTerm ":=" CoqTerm
+  syntax CoqCofixBodyList ::= List{CoqCofixBody, "with"}
+  syntax CoqCofixBodies ::= CoqCofixBody
+                          | CoqCofixBody CoqCofixBodyList "for" CoqIdent
+
+  syntax CoqMatchItem ::= CoqTerm
+                        | CoqTerm "as" CoqName
+  syntax CoqMatchItems ::= List{CoqMatchItem, ","} [klabel(CoqMatchItems)]
+
+  syntax CoqReturnType ::= "return" CoqTerm
+
+  syntax CoqEquation ::= CoqMultPattern "=>" CoqTerm
+                       | "|" CoqMultPattern "=>" CoqTerm
+  syntax CoqEquations ::= List{CoqEquation, "|"} [klabel(CoqEquations)]
+
+  syntax CoqPattern ::= CoqQualID CoqPattern
+                      | "@" CoqQualID CoqPattern
+                      // | CoqPattern CoqPattern
+                      | CoqPattern "as" CoqIdent
+                      | CoqPattern "%" CoqIdent
+                      | CoqQualID
+                      | Underscore [prefer]
+                      | Int
+
+  syntax CoqMultPattern ::= List{CoqPattern, ","} [klabel(CoqMultPattern)]
+  syntax CoqPatterns ::= NeList{CoqPattern, ""} [klabel(CoqPatterns)]
+
+// Vernacular
+  syntax CoqSentence ::= CoqDefinition
+                       | CoqInductive
+  //                   | CoqCoInductive
+  syntax CoqSentences ::= List{CoqSentence, ""} [klabel(CoqSentences), format(%1%n%2 %3)]
+  syntax CoqDefinition ::= "Definition" CoqIdent ":" CoqTerm ":=" CoqTerm "."
+//                         | "Definition" CoqIdent CoqBinders ":" CoqTerm ":=" CoqTerm "."
+
+  syntax CoqInductive ::= "Inductive" CoqIndBody "."
+  syntax CoqIndBody ::= CoqIdent CoqBinders ":" CoqTerm ":=" CoqIndCases
+  syntax CoqIndCase ::= CoqIdent CoqBinders ":" CoqTerm
+  syntax CoqIndCases ::= List{CoqIndCase, "|"} [klabel(CoqIndCases)]
+
+```
+
+```k
+endmodule
+```
diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md
index 6bf8c1062..43aae4bd6 100644
--- a/prover/lang/kore-lang.md
+++ b/prover/lang/kore-lang.md
@@ -9,6 +9,7 @@ module TOKENS
   syntax ColonName
   syntax PipeQID
   syntax Decimal
+  syntax Underscore
 
   // Abstract
   syntax Symbol ::= UpperName | LowerName
@@ -118,6 +119,7 @@ module TOKENS-SYNTAX
   syntax ColonName ::= r":[a-z][A-Za-z\\-0-9'\\#\\_]*" [token, autoReject]
   syntax Decimal ::= r"[0-9][0-9]*\\.[0-9][0-9]*" [token, autoreject]
                    | "2.0" [token]
+  syntax Underscore ::= "_" [token]
 endmodule
 
 module KORE
@@ -135,11 +137,13 @@ is to be used for generating fresh variables. *The second variety must be used
 only in this scenario*.
 
 ```k
-  syntax Variable ::= VariableName "{" Sort "}" [klabel(sortedVariable)]
+  syntax Variable    ::= VariableName  "{" Sort "}"  [klabel(sortedVariable)]
+  syntax SetVariable ::= "#" VariableName [klabel(setVariable)]
   syntax Pattern ::= Int
                    | Variable
+                   | SetVariable
                    | Symbol
-                   | Symbol "(" Patterns ")"                    [klabel(apply)]
+                   | Pattern "(" Patterns ")"                   [klabel(apply)]
 
                    | "\\top"    "(" ")"                         [klabel(top)]
                    | "\\bottom" "(" ")"                         [klabel(bottom)]
@@ -153,6 +157,9 @@ only in this scenario*.
                    | "\\exists" "{" Patterns "}" Pattern        [klabel(exists)]
                    | "\\forall" "{" Patterns "}" Pattern        [klabel(forall)]
 
+                   | "\\mu" "{" Patterns "}" Pattern            [klabel(mu)]
+                   | "\\nu" "{" Patterns "}" Pattern            [klabel(nu)]
+
                      /* Sugar for \iff, \mu and application */
                    | "\\iff-lfp" "(" Pattern "," Pattern ")"    [klabel(ifflfp)]
 
@@ -162,6 +169,11 @@ only in this scenario*.
                    | "heap" "(" Sort "," Sort ")" // Location, Data
                    | "\\hole" "(" ")" [klabel(Phole)]
 
+                   // for Coq translation
+                   | "\\lambda" "{" Patterns "}" Pattern        [klabel(lambda)]
+                   | "\\pi"     "{" Patterns "}" Pattern        [klabel(pi)]
+                   | "\\type" "(" Pattern "," Pattern ")"       [klabel(type)]
+
   rule \top()    => \and(.Patterns) [anywhere]
   rule \bottom() => \or(.Patterns) [anywhere]
 
@@ -207,6 +219,9 @@ module KORE-HELPERS
   syntax String ::= SortToString(Sort)     [function, functional, hook(STRING.token2string)]
   syntax String ::= SymbolToString(Symbol) [function, functional, hook(STRING.token2string)]
   syntax LowerName ::= StringToSymbol(String) [function, functional, hook(STRING.string2token)]
+  syntax UpperName ::= StringToSort(String) [function, functional, hook(STRING.string2token)]
+
+  syntax VariableName ::= StringToVariableName(String) [function, functional, hook(STRING.string2token)]
 
   syntax Symbol ::= parameterizedSymbol(Symbol, Sort) [function]
   rule parameterizedSymbol(SYMBOL, SORT) => StringToSymbol(SymbolToString(SYMBOL) +String "_" +String SortToString(SORT))
@@ -434,6 +449,10 @@ and values, passed to K's substitute.
   syntax Patterns ::= makeFreshVariables(Patterns) [function]
   rule makeFreshVariables(P, REST) => !V1:VariableName { getReturnSort(P) }, makeFreshVariables(REST)
   rule makeFreshVariables(.Patterns) => .Patterns
+
+  syntax Symbol ::= String2Symbol(String) [function, functional, hook(STRING.string2token)]
+  syntax Symbol ::= freshSymbol(Int) [freshGenerator, function, functional]
+  rule freshSymbol(I:Int) => String2Symbol("F" +String Int2String(I))
 ```
 
 ```k
diff --git a/prover/lang/smt-lang.md b/prover/lang/smt-lang.md
index e1a092d2a..f999a7d4a 100644
--- a/prover/lang/smt-lang.md
+++ b/prover/lang/smt-lang.md
@@ -103,6 +103,7 @@ module SMTLIB2-HELPERS
   imports K-IO
   imports SMTLIB2
   imports PROVER-CORE-SYNTAX
+  imports KORE-HELPERS
 
   syntax SMTLIB2AttributeValue ::=  CheckSATResult
   syntax CheckSATResult ::= "error" "(" K ")"
@@ -116,7 +117,6 @@ module SMTLIB2-HELPERS
 
 // Converting between Sorts:
 
-  syntax VariableName ::= StringToVariableName(String) [function, functional, hook(STRING.string2token)]
   syntax VariableName ::= SMTLIB2SimpleSymbolToVariableName(SMTLIB2SimpleSymbol) [function]
   rule SMTLIB2SimpleSymbolToVariableName(SYMBOL) => StringToVariableName("V" +String SMTLIB2SimpleSymbolToString(SYMBOL))
 
diff --git a/prover/prover b/prover/prover
index 4ba575218..031dd38e4 100755
--- a/prover/prover
+++ b/prover/prover
@@ -18,6 +18,12 @@ KDefinition( proj
            , directory = proj.builddir('defn/prover-smt')
            , krun_flags = '--interpret'
            )
+KDefinition( proj
+           , alias = 'prover-coq'
+           , backend = 'ocaml'
+           , directory = proj.builddir('defn/prover-coq')
+           , krun_flags = '--interpret'
+           )
 KDefinition( proj
            , alias = 'test-driver'
            , backend = 'llvm'
diff --git a/prover/prover.md b/prover/prover.md
index 8b928190d..834c3b44e 100644
--- a/prover/prover.md
+++ b/prover/prover.md
@@ -1,5 +1,7 @@
 ```k
 requires "lang/kore-lang.k"
+requires "lang/coq-lang.k"
+requires "drivers/coq-driver.k"
 requires "drivers/smt-driver.k"
 requires "drivers/kore-driver.k"
 requires "drivers/base.k"
@@ -11,6 +13,7 @@ requires "strategies/intros.k"
 requires "strategies/knaster-tarski.k"
 requires "strategies/matching.k"
 requires "strategies/search-bound.k"
+requires "strategies/typecheck.k"
 requires "strategies/simplification.k"
 requires "strategies/smt.k"
 requires "strategies/reflexivity.k"
@@ -68,6 +71,7 @@ module STRATEGIES-EXPORTED-SYNTAX
                         "in:" AxiomName ","
                         "vars:" VariableNames ","
                         "with:" Patterns ")"
+                    | "typecheck"
 
   syntax RewriteDirection ::= "->" | "<-"
 
diff --git a/prover/strategies/typecheck.md b/prover/strategies/typecheck.md
new file mode 100644
index 000000000..73604058d
--- /dev/null
+++ b/prover/strategies/typecheck.md
@@ -0,0 +1,34 @@
+# typecheck - for Coq terms
+
+```k
+module STRATEGY-TYPECHECK
+  imports PROVER-CORE
+  imports STRATEGIES-EXPORTED-SYNTAX
+
+  rule
+    <claim> \type(ID:Symbol, TYPE) => \type(TERM, TYPE) </claim>
+    <strategy> typecheck ... </strategy>
+    <declaration> axiom AXID : \equals(ID, TERM) </declaration>
+
+  rule
+    <claim> \type(TYPE, TYPE) </claim>
+    <strategy> typecheck => success ... </strategy>
+
+  // axiom: (Term, Term, Term)
+  // TODO: use Term as constant
+  rule
+    <claim> \type(\pi { VARs } TYPE, #token("Term", "UpperName")) </claim>
+    <strategy> typecheck => success ... </strategy>
+
+  // lambda
+  rule
+    <claim> \type(\lambda { VARs1 } TERM, \pi { VARs2 } TYPE) => \type(TERM, TYPE) </claim>
+    <strategy> typecheck ... </strategy>
+
+  // application
+  rule
+    <claim> \type(TERM1 ( TERM2 ), TYPE) => \type(TERM1, \pi { !X:VariableName { #token("Term", "UpperName") } } TYPE) </claim>
+    <strategy> typecheck ... </strategy>
+
+endmodule
+```
diff --git a/prover/t/coq-tests/Logic.v b/prover/t/coq-tests/Logic.v
new file mode 100644
index 000000000..42c98d955
--- /dev/null
+++ b/prover/t/coq-tests/Logic.v
@@ -0,0 +1,46 @@
+// Inductive True : Prop :=
+//   I : True .
+
+// Inductive False : Prop := .
+
+// Inductive nat : Prop :=
+//     Z : nat
+//   | S : (forall (x : nat), nat) .
+
+Definition not : (forall (x : Prop), Prop) :=
+  fun (A: Prop) => (forall (x : A), False) .
+
+Definition iff : (forall (x : Prop), (forall (y : Prop), Prop)) :=
+  (and (forall (x : A), B)) (forall (y : B), A) .
+
+Definition IF_then_else : (forall (x : Prop), (forall (y : Prop), (forall (z : Prop), Prop))) :=
+  (or (and P Q)) (and (not P) R) .
+
+// Inductive ex1 (A : Type) (P : forall (x : A), Prop) : Prop :=
+//   ex_intro1 : forall (x : A), forall (y : (P x)), ex1 A P .
+ 
+// Inductive ex2 (A : Type) (P : forall (x : A), Prop) : Prop :=
+//   ex_intro2 : forall (x : A), forall (y : (P x)), ex2 P .
+
+// // Inductive ex3 (A : Type) (P : forall (x : A), Prop) : Prop :=
+// //   ex_intro3 : forall (x : A), forall (y : (P x)), ex3 (A:=A) P .
+
+// Inductive ex4 (A : Type) (P : forall (x : A), Prop) : Prop :=
+//   ex_intro4 : forall (x : A), forall (y : (P x)), @ ex4 A P .
+
+Definition AndComm : (forall (A B : Prop), (forall (c : and A B), and B A)) :=
+  fun (A B : Prop) (H : and A B) =>
+    match H with
+      conj H0 H1 => conj H1 H0
+    end
+  .
+
+// // Inductive and (A B : Prop) : Prop :=
+// //   conj : forall (x : A), forall (y : B), and A B .
+// // 
+// // Inductive or (A B : Prop) : Prop :=
+// //     or_introl : forall (x : A), or A B
+// //   | or_intror : forall (y : A), or A B .
+// // 
+// // Inductive eq (A:Type) (x:A) : forall (_:A), Prop :=
+// //     eq_refl : @ eq A x x .
diff --git a/prover/t/coq-tests/Logic.v.expected b/prover/t/coq-tests/Logic.v.expected
new file mode 100644
index 000000000..e70bbc419
--- /dev/null
+++ b/prover/t/coq-tests/Logic.v.expected
@@ -0,0 +1,84 @@
+<prover>
+  <k>
+    .CoqSentences
+  </k>
+  <exit-code>
+    1
+  </exit-code>
+  <goals>
+    .GoalCellSet
+  </goals>
+  <declarations>
+    <declaration>
+      axiom \equals ( AndComm , \lambda { A { Term } , B { Term } , H { Term } , .Patterns } \or ( \exists { H0 , H1 , .Patterns } \and ( \equals ( H , conj ( H0 , H1 , .Patterns ) ) , conj ( H1 , H0 , .Patterns ) , .Patterns ) , .Patterns ) )
+    </declaration> <declaration>
+      axiom \equals ( IF_then_else , or ( and , P , Q , .Patterns ) ( and , not , P , R , .Patterns ) )
+    </declaration> <declaration>
+      axiom \equals ( iff , and ( \forall { x { Term } , .Patterns } B , .Patterns ) ( \forall { y { Term } , .Patterns } A , .Patterns ) )
+    </declaration> <declaration>
+      axiom \equals ( not , \lambda { A { Term } , .Patterns } \forall { x { Term } , .Patterns } False )
+    </declaration> <declaration>
+      axiom \type ( I ( .Patterns ) , True )
+    </declaration> <declaration>
+      axiom \type ( S ( .Patterns ) , nat ( - , > , nat , .Patterns ) )
+    </declaration> <declaration>
+      axiom \type ( Z ( .Patterns ) , nat )
+    </declaration> <declaration>
+      axiom \type ( conj ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( and ( A , B , .Patterns ) ) )
+    </declaration> <declaration>
+      axiom \type ( ex_intro1 ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( ex1 ( A , P , .Patterns ) ) )
+    </declaration> <declaration>
+      axiom \type ( ex_intro2 ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( ex2 ( P , .Patterns ) ) )
+    </declaration> <declaration>
+      axiom \type ( ex_intro4 ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( ex4 ( A , .Patterns ) ( P , .Patterns ) ) )
+    </declaration> <declaration>
+      axiom \type ( or_introl ( .Patterns ) , \forall { x { Term } , .Patterns } ( or ( A , B , .Patterns ) ) )
+    </declaration> <declaration>
+      axiom \type ( or_intror ( .Patterns ) , \forall { y { Term } , .Patterns } ( or ( A , B , .Patterns ) ) )
+    </declaration> <declaration>
+      sort Term
+    </declaration> <declaration>
+      symbol AndComm ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol False ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol I ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol IF_then_else ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol S ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol True ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol Z ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol and ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol conj ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol ex1 ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol ex2 ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol ex4 ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol ex_intro1 ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol ex_intro2 ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol ex_intro4 ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol iff ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol nat ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol not ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol or ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol or_introl ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol or_intror ( .Sorts ) : Term
+    </declaration>
+  </declarations>
+</prover>
diff --git a/prover/t/coq-tests/ml_coq_verbose.v b/prover/t/coq-tests/ml_coq_verbose.v
new file mode 100644
index 000000000..875648b29
--- /dev/null
+++ b/prover/t/coq-tests/ml_coq_verbose.v
@@ -0,0 +1,75 @@
+Inductive and' (A B : Prop) : Prop :=
+    conj' : forall (_ : A) (_ : B), and' A B .
+
+Definition and'_ind_verbose : forall (A B P : Prop) (_ : forall (_ : A) (_ : B), P)(_ : and' A B), P := 
+fun (A B P : Prop) (f : forall (_ : A) (_ : B), P) (a : and' A B) =>
+match a return P with
+| conj' _ _ x x0 => f x x0
+end .
+
+Definition and'_rec_verbose : forall (A B : Prop) (P : Set) (_ : forall (_ : A) (_ : B), P)(_ : and' A B), P := 
+fun (A B : Prop) (P : Set) => and'_rect A B P .
+
+Definition and'_rect_verbose : forall (A B : Prop) (P : Type) (_ : forall (_ : A) (_ : B), P)(_ : and' A B), P := 
+fun (A B : Prop) (P : Type) (f : forall (_ : A) (_ : B), P)
+  (a : and' A B) =>
+match a return P with
+| conj' _ _ x x0 => f x x0
+end .
+
+Inductive ex1 (A : Type) (P : forall (_ : A), Prop) : Prop :=
+    ex_intro1 : forall (x : A) (_ : P x), ex1 A P .
+
+Definition ex1_ind_verbose : forall (A : Type) (P : forall (_ : A), Prop)(P0 : Prop) (_ : forall (x : A) (_ : P x), P0)(_ : ex1 A P), P0 := 
+fun (A : Type) (P : forall (_ : A), Prop) (P0 : Prop)
+  (f : forall (x : A) (_ : P x), P0) (e : ex1 A P) =>
+match e return P0 with
+| ex_intro1 _ _ x x0 => f x x0
+end .
+
+Definition False_ind : forall (P : Prop) (_ : False), P := 
+fun (P : Prop) (f : False) => match f return P with
+                              end .
+
+Definition add_ind' : forall (_ : nat) (_ : nat), nat := 
+fix add (n m : nat) {struct n} : nat :=
+  match n return nat with
+  | O => m
+  | S p => S (add p m)
+  end .
+
+Definition nat_ind' : forall (P : forall (_ : nat), Prop) (_ : P O)(_ : forall (n : nat) (_ : P n), P (S n))(n : nat), P n := 
+fun (P : forall (_ : nat), Prop) (f : P O)
+  (f0 : forall (n : nat) (_ : P n), P (S n)) =>
+fix F (n : nat) : P n :=
+  match n as n0 return (P n0) with
+  | O => f
+  | S n0 => f0 n0 (F n0)
+  end .
+
+Definition AddZero : forall (n : nat), @eq nat (Nat.add n O) n := 
+fun (n : nat) =>
+nat_ind (fun (n0 : nat) => @eq nat (Nat.add n0 O) n0)
+  (@eq_refl nat O : @eq nat (Nat.add O O) O)
+  (fun (n0 : nat) (IHn : @eq nat (Nat.add n0 O) n0) =>
+   @eq_ind_r nat n0 (fun (n1 : nat) => @eq nat (S n1) (S n0))
+     (@eq_refl nat (S n0)) (Nat.add n0 O) IHn
+   :
+   @eq nat (Nat.add (S n0) O) (S n0)) n .
+
+Definition AndComm : forall (A B : Prop) (_ : and A B), and B A := 
+fun (A B : Prop) (H : and A B) =>
+match H return (and B A) with
+| conj H0 H1 => @conj B A H1 H0
+end .
+
+Definition AndComm' : forall (A B : Prop) (_ : and A B), and B A := 
+fun (A B : Prop) (H : and A B) =>
+match H return (and B A) with
+| conj H0 H1 => @conj B A H1 H0
+end .
+
+Definition AndComm'' : forall (A B : Prop) (_ : and A B), and B A := 
+AndComm' .
+  
+Definition test : forall (_ : Prop), Prop := fun (_ : Prop) => True .
diff --git a/prover/t/coq-tests/nat_ind.v b/prover/t/coq-tests/nat_ind.v
new file mode 100644
index 000000000..f3c9036b3
--- /dev/null
+++ b/prover/t/coq-tests/nat_ind.v
@@ -0,0 +1,22 @@
+Inductive nat : Type :=  Z : nat | S : forall (x : nat), nat .
+
+// symbol nat() : Term
+// symbol Z() : Term
+// symbol S() : Term
+
+// axiom \type(Z(), nat())
+
+Definition nat_ind : (forall (P : (forall (x : nat), Prop)),
+                     (forall (y : P 0),
+                     (forall (l : (forall (n : nat),
+                                  (forall (y : P n), P (S n)))),
+                             (forall (n : nat), P n)))) := 
+fun (P : (forall (n : nat), Prop)) (f : P 0) (f0 : forall (n : nat), (forall (x : P n), P (S n))) =>
+fix F (n : nat) := match n with
+                           Z => f
+                         | S n0 => f0 n0 (F n0)
+                   end
+.
+
+// forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
+// tr(fun ... ) \mu { F {{ Term }} } tr( fun n => match ) ... )
diff --git a/prover/t/coq-tests/nat_ind.v.expected b/prover/t/coq-tests/nat_ind.v.expected
new file mode 100644
index 000000000..d64c4c59b
--- /dev/null
+++ b/prover/t/coq-tests/nat_ind.v.expected
@@ -0,0 +1,30 @@
+<prover>
+  <k>
+    .CoqSentences
+  </k>
+  <exit-code>
+    1
+  </exit-code>
+  <goals>
+    .GoalCellSet
+  </goals>
+  <declarations>
+    <declaration>
+      axiom \equals ( nat_ind , \lambda { P { Term } , f { Term } , f0 { Term } , .Patterns } \mu { F {{ Term }} , .Patterns } \lambda { n { Term } , .Patterns } \or ( \exists { .Patterns } \and ( \equals ( n , Z ) , f , .Patterns ) , \exists { n0 , .Patterns } \and ( \equals ( n , S ( n0 , .Patterns ) ) , f0 ( n0 , F , n0 , .Patterns ) , .Patterns ) , .Patterns ) )
+    </declaration> <declaration>
+      axiom \type ( S ( .Patterns ) , \forall { x { Term } , .Patterns } nat )
+    </declaration> <declaration>
+      axiom \type ( Z ( .Patterns ) , nat )
+    </declaration> <declaration>
+      sort Term
+    </declaration> <declaration>
+      symbol S ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol Z ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol nat ( .Sorts ) : Term
+    </declaration> <declaration>
+      symbol nat_ind ( .Sorts ) : Term
+    </declaration>
+  </declarations>
+</prover>