diff --git a/Makefile b/Makefile
index ff9fa4d72..89c43c460 100644
--- a/Makefile
+++ b/Makefile
@@ -1,25 +1,29 @@
-all: template-coq checker
+all: template-coq checker extraction
 
 .PHONY: all template-coq checker install html clean mrproper .merlin test-suite translations
 
 install: 
 	$(MAKE) -C template-coq install
 	$(MAKE) -C checker install
+	$(MAKE) -C extraction install
 
 html: all
 	$(MAKE) -C template-coq html
+	$(MAKE) -C extraction html
 	mv template-coq/html/*.html html
 	rm template-coq/html/coqdoc.css
 	rm -d template-coq/html
 
 clean:
 	$(MAKE) -C template-coq clean
+	$(MAKE) -C extraction clean
 	$(MAKE) -C checker clean
 	$(MAKE) -C test-suite clean
 	$(MAKE) -C translations clean
 
 mrproper:
 	$(MAKE) -C template-coq mrproper
+	$(MAKE) -C extraction mrproper
 	$(MAKE) -C checker mrproper
 
 .merlin:
@@ -29,6 +33,9 @@ mrproper:
 template-coq:
 	$(MAKE) -C template-coq
 
+extraction: template-coq
+	$(MAKE) -C extraction
+
 checker: template-coq
 	./movefiles.sh
 	$(MAKE) -C checker
diff --git a/extraction/Makefile b/extraction/Makefile
new file mode 100644
index 000000000..4604b2291
--- /dev/null
+++ b/extraction/Makefile
@@ -0,0 +1,799 @@
+###############################################################################
+##  v      #                   The Coq Proof Assistant                       ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                   ##
+##   \VV/  #                                                                 ##
+##    //   #                                                                 ##
+###############################################################################
+## GNUMakefile for Coq 8.8.1
+
+# For debugging purposes (must stay here, don't move below)
+INITIAL_VARS := $(.VARIABLES)
+# To implement recursion we save the name of the main Makefile
+SELF := $(lastword $(MAKEFILE_LIST))
+PARENT := $(firstword $(MAKEFILE_LIST))
+
+# This file is generated by coq_makefile and contains many variable
+# definitions, like the list of .v files or the path to Coq
+include Makefile.conf
+
+# Put in place old names
+VFILES            := $(COQMF_VFILES)
+MLIFILES          := $(COQMF_MLIFILES)
+MLFILES           := $(COQMF_MLFILES)
+ML4FILES          := $(COQMF_ML4FILES)
+MLPACKFILES       := $(COQMF_MLPACKFILES)
+MLLIBFILES        := $(COQMF_MLLIBFILES)
+CMDLINE_VFILES    := $(COQMF_CMDLINE_VFILES)
+INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
+OTHERFLAGS        := $(COQMF_OTHERFLAGS)
+COQ_SRC_SUBDIRS   := $(COQMF_COQ_SRC_SUBDIRS)
+OCAMLLIBS         := $(COQMF_OCAMLLIBS)
+SRC_SUBDIRS       := $(COQMF_SRC_SUBDIRS)
+COQLIBS           := $(COQMF_COQLIBS)
+COQLIBS_NOML      := $(COQMF_COQLIBS_NOML)
+CMDLINE_COQLIBS   := $(COQMF_CMDLINE_COQLIBS)
+LOCAL             := $(COQMF_LOCAL)
+COQLIB            := $(COQMF_COQLIB)
+DOCDIR            := $(COQMF_DOCDIR)
+OCAMLFIND         := $(COQMF_OCAMLFIND)
+CAMLP5O           := $(COQMF_CAMLP5O)
+CAMLP5BIN         := $(COQMF_CAMLP5BIN)
+CAMLP5LIB         := $(COQMF_CAMLP5LIB)
+CAMLP5OPTIONS     := $(COQMF_CAMLP5OPTIONS)
+CAMLFLAGS         := $(COQMF_CAMLFLAGS)
+HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
+
+Makefile.conf: _CoqProject
+	coq_makefile -o Makefile -f _CoqProject
+
+# This file can be created by the user to hook into double colon rules or
+# add any other Makefile code he may need
+-include Makefile.local
+
+# Parameters ##################################################################
+#
+# Parameters are make variable assignments.
+# They can be passed to (each call to) make on the command line.
+# They can also be put in Makefile.local once an for all.
+# For retro-compatibility reasons they can be put in the _CoqProject, but this
+# practice is discouraged since _CoqProject better not contain make specific
+# code (be nice to user interfaces).
+
+# Print shell commands (set to non empty)
+VERBOSE ?=
+
+# Time the Coq process (set to non empty), and how (see default value)
+TIMED?=
+TIMECMD?=
+# Use /usr/bin/env time on linux, gtime on Mac OS
+TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+ifneq (,$(TIMED))
+ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=/usr/bin/env time -f $(TIMEFMT)
+else
+ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=gtime -f $(TIMEFMT)
+else
+STDTIME?=time
+endif
+endif
+else
+STDTIME?=/usr/bin/env time -f $(TIMEFMT)
+endif
+
+# Coq binaries
+COQC     ?= "$(COQBIN)coqc"
+COQTOP   ?= "$(COQBIN)coqtop"
+COQCHK   ?= "$(COQBIN)coqchk"
+COQDEP   ?= "$(COQBIN)coqdep"
+GALLINA  ?= "$(COQBIN)gallina"
+COQDOC   ?= "$(COQBIN)coqdoc"
+COQMKFILE ?= "$(COQBIN)coq_makefile"
+
+# Timing scripts
+COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
+COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
+COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py"
+BEFORE ?=
+AFTER ?=
+
+# FIXME this should be generated by Coq (modules already linked by Coq)
+CAMLDONTLINK=camlp5.gramlib,unix,str
+
+# OCaml binaries
+CAMLC       ?= "$(OCAMLFIND)" ocamlc   -c
+CAMLOPTC    ?= "$(OCAMLFIND)" opt      -c
+CAMLLINK    ?= "$(OCAMLFIND)" ocamlc   -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLOPTLINK ?= "$(OCAMLFIND)" opt      -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLDOC     ?= "$(OCAMLFIND)" ocamldoc
+CAMLDEP     ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
+
+# DESTDIR is prepended to all installation paths
+DESTDIR ?=
+
+# Debug builds, typically -g to OCaml, -debug to Coq.
+CAMLDEBUG ?=
+COQDEBUG ?=
+
+# Extra packages to be linked in (as in findlib -package)
+CAMLPKGS ?=
+
+# Option for making timing files
+TIMING?=
+# Option for changing sorting of timing output file
+TIMING_SORT_BY ?= auto
+# Output file names for timed builds
+TIME_OF_BUILD_FILE               ?= time-of-build.log
+TIME_OF_BUILD_BEFORE_FILE        ?= time-of-build-before.log
+TIME_OF_BUILD_AFTER_FILE         ?= time-of-build-after.log
+TIME_OF_PRETTY_BUILD_FILE        ?= time-of-build-pretty.log
+TIME_OF_PRETTY_BOTH_BUILD_FILE   ?= time-of-build-both.log
+TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
+
+########## End of parameters ##################################################
+# What follows may be relevant to you only if you need to
+# extend this Makefile.  If so, look for 'Extension point' here and
+# put in Makefile.local double colon rules accordingly.
+# E.g. to perform some work after the all target completes you can write
+#
+# post-all::
+# 	echo "All done!"
+#
+# in Makefile.local
+#
+###############################################################################
+
+
+
+
+# Flags #######################################################################
+#
+# We define a bunch of variables combining the parameters
+
+SHOW := $(if $(VERBOSE),@true "",@echo "")
+HIDE := $(if $(VERBOSE),,@)
+
+TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
+
+OPT?=
+
+# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
+ifeq '$(OPT)' '-byte'
+USEBYTE:=true
+DYNOBJ:=.cma
+DYNLIB:=.cma
+else
+USEBYTE:=
+DYNOBJ:=.cmxs
+DYNLIB:=.cmxs
+endif
+
+COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
+COQCHKFLAGS?=-silent -o $(COQLIBS)
+COQDOCFLAGS?=-interpolate -utf8
+COQDOCLIBS?=$(COQLIBS_NOML)
+
+# The version of Coq being run and the version of coq_makefile that
+# generated this makefile
+COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
+COQMAKEFILE_VERSION:=8.8.1
+
+COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
+
+CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB)
+
+# ocamldoc fails with unknown argument otherwise
+CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+
+# FIXME This should be generated by Coq
+GRAMMARS:=grammar.cma
+CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
+
+CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null)
+ifeq (,$(CAMLLIB))
+PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.")
+else
+PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl'
+endif
+
+ifneq (,$(TIMING))
+TIMING_ARG=-time
+ifeq (after,$(TIMING))
+TIMING_EXT=after-timing
+else
+ifeq (before,$(TIMING))
+TIMING_EXT=before-timing
+else
+TIMING_EXT=timing
+endif
+endif
+else
+TIMING_ARG=
+endif
+
+# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
+ifdef DSTROOT
+DESTDIR := $(DSTROOT)
+endif
+
+concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2))
+
+COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib)
+COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib)
+COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop)
+
+# Files #######################################################################
+#
+# We here define a bunch of variables about the files being part of the
+# Coq project in order to ease the writing of build target and build rules
+
+VDFILE := .coqdeps
+
+ALLSRCFILES := \
+	$(ML4FILES) \
+	$(MLFILES) \
+	$(MLPACKFILES) \
+	$(MLLIBFILES) \
+	$(MLIFILES)
+
+# helpers
+vo_to_obj = $(addsuffix .o,\
+  $(filter-out Warning: Error:,\
+  $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1))))
+strip_dotslash = $(patsubst ./%,%,$(1))
+VO = vo
+
+VOFILES = $(VFILES:.v=.$(VO))
+GLOBFILES = $(VFILES:.v=.glob)
+GFILES = $(VFILES:.v=.g)
+HTMLFILES = $(VFILES:.v=.html)
+GHTMLFILES = $(VFILES:.v=.g.html)
+BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
+TEXFILES = $(VFILES:.v=.tex)
+GTEXFILES = $(VFILES:.v=.g.tex)
+CMOFILES = \
+	$(ML4FILES:.ml4=.cmo) \
+	$(MLFILES:.ml=.cmo) \
+	$(MLPACKFILES:.mlpack=.cmo)
+CMXFILES = $(CMOFILES:.cmo=.cmx)
+OFILES = $(CMXFILES:.cmx=.o)
+CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma)
+CMXAFILES = $(CMAFILES:.cma=.cmxa)
+CMIFILES = \
+	$(CMOFILES:.cmo=.cmi) \
+	$(MLIFILES:.mli=.cmi)
+# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just
+# a .ml4 file
+CMXSFILES = \
+	$(MLPACKFILES:.mlpack=.cmxs) \
+	$(CMXAFILES:.cmxa=.cmxs) \
+	$(if $(MLPACKFILES)$(CMXAFILES),,\
+		$(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs))
+
+# files that are packed into a plugin (no extension)
+PACKEDFILES = \
+	$(call strip_dotslash, \
+	  $(foreach lib, \
+            $(call strip_dotslash, \
+	       $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib))))
+# files that are archived into a .cma (mllib)
+LIBEDFILES = \
+	$(call strip_dotslash, \
+	  $(foreach lib, \
+            $(call strip_dotslash, \
+	       $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib))))
+CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES))
+CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES))
+OBJFILES = $(call vo_to_obj,$(VOFILES))
+ALLNATIVEFILES = \
+	$(OBJFILES:.o=.cmi) \
+	$(OBJFILES:.o=.cmx) \
+	$(OBJFILES:.o=.cmxs)
+# trick: wildcard filters out non-existing files, so that `install` doesn't show
+# warnings and `clean` doesn't pass to rm a list of files that is too long for
+# the shell.
+NATIVEFILES = $(wildcard $(ALLNATIVEFILES))
+FILESTOINSTALL = \
+	$(VOFILES) \
+	$(VFILES) \
+	$(GLOBFILES) \
+	$(NATIVEFILES) \
+	$(CMIFILESTOINSTALL)
+BYTEFILESTOINSTALL = \
+	$(CMOFILESTOINSTALL) \
+	$(CMAFILES)
+ifeq '$(HASNATDYNLINK)' 'true'
+DO_NATDYNLINK = yes
+FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx)
+else
+DO_NATDYNLINK =
+endif
+
+ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE))
+
+# Compilation targets #########################################################
+
+all:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
+.PHONY: all
+
+all.timing.diff:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES=""
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
+.PHONY: all.timing.diff
+
+make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE)
+make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE)
+make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
+	$(HIDE)rm -f pretty-timed-success.ok
+	$(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE)
+	$(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed
+print-pretty-timed::
+	$(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+print-pretty-timed-diff::
+	$(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ifeq (,$(BEFORE))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	$(HIDE)false
+else
+ifeq (,$(AFTER))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	$(HIDE)false
+else
+print-pretty-single-time-diff::
+	$(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+endif
+endif
+pretty-timed:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed
+.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff
+
+# Extension points for actions to be performed before/after the all target
+pre-all::
+	@# Extension point
+	$(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\
+	  echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\
+	  echo "W: while the current Coq version is $(COQ_VERSION)";\
+	fi
+.PHONY: pre-all
+
+post-all::
+	@# Extension point
+.PHONY: post-all
+
+real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles)
+.PHONY: real-all
+
+real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff)
+.PHONY: real-all.timing.diff
+
+bytefiles: $(CMOFILES) $(CMAFILES)
+.PHONY: bytefiles
+
+optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
+.PHONY: optfiles
+
+# FIXME, see Ralf's bugreport
+quick: $(VOFILES:.vo=.vio)
+.PHONY: quick
+
+vio2vo:
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
+		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
+.PHONY: vio2vo
+
+quick2vo:
+	$(HIDE)make -j $(J) quick
+	$(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
+	  viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
+	  if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
+	done); \
+	echo "VIO2VO: $$VIOFILES"; \
+	if [ -n "$$VIOFILES" ]; then \
+	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \
+	fi
+.PHONY: quick2vo
+
+checkproofs:
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
+		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
+.PHONY: checkproofs
+
+validate: $(VOFILES)
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $^
+.PHONY: validate
+
+only: $(TGTS)
+.PHONY: only
+
+# Documentation targets #######################################################
+
+html: $(GLOBFILES) $(VFILES)
+	$(SHOW)'COQDOC -d html $(GAL)'
+	$(HIDE)mkdir -p html
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
+
+mlihtml: $(MLIFILES:.mli=.cmi)
+	$(SHOW)'CAMLDOC -d $@'
+	$(HIDE)mkdir $@ || rm -rf $@/*
+	$(HIDE)$(CAMLDOC) -html \
+		-d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
+
+all-mli.tex: $(MLIFILES:.mli=.cmi)
+	$(SHOW)'CAMLDOC -latex $@'
+	$(HIDE)$(CAMLDOC) -latex \
+		-o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
+
+gallina: $(GFILES)
+
+all.ps: $(VFILES)
+	$(SHOW)'COQDOC -ps $(GAL)'
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \
+		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all.pdf: $(VFILES)
+	$(SHOW)'COQDOC -pdf $(GAL)'
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
+		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+# FIXME: not quite right, since the output name is different
+gallinahtml: GAL=-g
+gallinahtml: html
+
+all-gal.ps: GAL=-g
+all-gal.ps: all.ps
+
+all-gal.pdf: GAL=-g
+all-gal.pdf: all.pdf
+
+# ?
+beautify: $(BEAUTYFILES)
+	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
+	@echo 'Do not do "make clean" until you are sure that everything went well!'
+	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
+.PHONY: beautify
+
+# Installation targets ########################################################
+#
+# There rules can be extended in Makefile.local
+# Extensions can't assume when they run.
+
+install:
+	$(HIDE)for f in $(FILESTOINSTALL); do\
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ "$$?" != "0" -o -z "$$df" ]; then\
+	   echo SKIP "$$f" since it has no logical path;\
+	 else\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
+	 fi;\
+	done
+	$(HIDE)$(MAKE) install-extra -f "$(SELF)"
+install-extra::
+	@# Extension point
+.PHONY: install install-extra
+
+install-byte:
+	$(HIDE)for f in $(BYTEFILESTOINSTALL); do\
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ "$$?" != "0" -o -z "$$df" ]; then\
+	   echo SKIP "$$f" since it has no logical path;\
+	 else\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
+	 fi;\
+	done
+
+install-doc:: html mlihtml
+	@# Extension point
+	$(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(HIDE)for i in html/*; do \
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 install -m 0644 "$$i" "$$dest";\
+	 echo INSTALL "$$i" "$$dest";\
+	done
+	$(HIDE)install -d \
+		"$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE)for i in mlihtml/*; do \
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 install -m 0644 "$$i" "$$dest";\
+	 echo INSTALL "$$i" "$$dest";\
+	done
+.PHONY: install-doc
+
+uninstall::
+	@# Extension point
+	$(HIDE)for f in $(FILESTOINSTALL); do \
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
+	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
+	 rm -f "$$instf" &&\
+	 echo RM "$$instf" &&\
+	 (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
+	done
+.PHONY: uninstall
+
+uninstall-doc::
+	@# Extension point
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
+.PHONY: uninstall-doc
+
+# Cleaning ####################################################################
+#
+# There rules can be extended in Makefile.local
+# Extensions can't assume when they run.
+
+clean::
+	@# Extension point
+	$(SHOW)'CLEAN'
+	$(HIDE)rm -f $(CMOFILES)
+	$(HIDE)rm -f $(CMIFILES)
+	$(HIDE)rm -f $(CMAFILES)
+	$(HIDE)rm -f $(CMOFILES:.cmo=.cmx)
+	$(HIDE)rm -f $(CMXAFILES)
+	$(HIDE)rm -f $(CMXSFILES)
+	$(HIDE)rm -f $(CMOFILES:.cmo=.o)
+	$(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
+	$(HIDE)rm -f $(ALLDFILES)
+	$(HIDE)rm -f $(NATIVEFILES)
+	$(HIDE)find . -name .coq-native -type d -empty -delete
+	$(HIDE)rm -f $(VOFILES)
+	$(HIDE)rm -f $(VOFILES:.vo=.vio)
+	$(HIDE)rm -f $(GFILES)
+	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
+	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
+	$(HIDE)rm -f $(VFILES:.v=.glob)
+	$(HIDE)rm -f $(VFILES:.v=.tex)
+	$(HIDE)rm -f $(VFILES:.v=.g.tex)
+	$(HIDE)rm -f pretty-timed-success.ok
+	$(HIDE)rm -rf html mlihtml
+.PHONY: clean
+
+cleanall:: clean
+	@# Extension point
+	$(SHOW)'CLEAN *.aux *.timing'
+	$(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
+	$(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.before-timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.after-timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff)
+.PHONY: cleanall
+
+archclean::
+	@# Extension point
+	$(SHOW)'CLEAN *.cmx *.o'
+	$(HIDE)rm -f $(NATIVEFILES)
+	$(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx)
+.PHONY: archclean
+
+
+# Compilation rules ###########################################################
+
+$(MLIFILES:.mli=.cmi): %.cmi: %.mli
+	$(SHOW)'CAMLC -c $<'
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+
+$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4
+	$(SHOW)'CAMLC -pp -c $<'
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $<
+
+$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4
+	$(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<'
+	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $<
+
+$(MLFILES:.ml=.cmo): %.cmo: %.ml
+	$(SHOW)'CAMLC -c $<'
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+
+$(MLFILES:.ml=.cmx): %.cmx: %.ml
+	$(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
+	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
+
+
+$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
+	$(SHOW)'CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-linkall -shared -o $@ $<
+
+$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
+	$(SHOW)'CAMLC -a -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
+	$(SHOW)'CAMLOPT -a -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+
+$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
+	$(SHOW)'CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-shared -linkall -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
+	$(SHOW)'CAMLOPT -a -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
+	$(SHOW)'CAMLC -a -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
+	$(SHOW)'CAMLC -pack -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+
+$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
+	$(SHOW)'CAMLOPT -pack -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+
+# This rule is for _CoqProject with no .mllib nor .mlpack
+$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx
+	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-shared -o $@ $<
+
+ifneq (,$(TIMING))
+TIMING_EXTRA = > $<.$(TIMING_EXT)
+else
+TIMING_EXTRA =
+endif
+
+$(VOFILES): %.vo: %.v
+	$(SHOW)COQC $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA)
+
+# FIXME ?merge with .vo / .vio ?
+$(GLOBFILES): %.glob: %.v
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $<
+
+$(VFILES:.v=.vio): %.vio: %.v
+	$(SHOW)COQC -quick $<
+	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
+
+$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
+	$(SHOW)PYTHON TIMING-DIFF $<
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
+
+$(BEAUTYFILES): %.v.beautified: %.v
+	$(SHOW)'BEAUTIFY $<'
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
+
+$(GFILES): %.g: %.v
+	$(SHOW)'GALLINA $<'
+	$(HIDE)$(GALLINA) $<
+
+$(TEXFILES): %.tex: %.v
+	$(SHOW)'COQDOC -latex $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
+
+$(GTEXFILES): %.g.tex: %.v
+	$(SHOW)'COQDOC -latex -g $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
+
+$(HTMLFILES): %.html: %.v %.glob
+	$(SHOW)'COQDOC -html $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
+
+$(GHTMLFILES): %.g.html: %.v %.glob
+	$(SHOW)'COQDOC -html -g $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
+
+# Dependency files ############################################################
+
+ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),)
+ -include $(ALLDFILES)
+else
+ ifeq ($(MAKECMDGOALS),)
+  -include $(ALLDFILES)
+ endif
+endif
+
+.SECONDARY: $(ALLDFILES)
+
+redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV )
+
+$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4
+	$(SHOW)'CAMLDEP -pp $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+
+# If this makefile is created using a _CoqProject we have coqdep get
+# options from it. This avoids argument length limits for pathological
+# projects. Note that extra options might be on the command line.
+VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES)
+
+$(VDFILE).d: $(VFILES)
+	$(SHOW)'COQDEP VFILES'
+	$(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
+
+# Misc ########################################################################
+
+byte:
+	$(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)"
+.PHONY: byte
+
+opt:
+	$(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)"
+.PHONY:	opt
+
+# This is deprecated.  To extend this makefile use
+# extension points and Makefile.local
+printenv::
+	$(warning printenv is deprecated)
+	$(warning write extensions in Makefile.local or include Makefile.conf)
+	@echo 'LOCAL = $(LOCAL)'
+	@echo 'COQLIB = $(COQLIB)'
+	@echo 'DOCDIR = $(DOCDIR)'
+	@echo 'OCAMLFIND = $(OCAMLFIND)'
+	@echo 'CAMLP5O = $(CAMLP5O)'
+	@echo 'CAMLP5BIN = $(CAMLP5BIN)'
+	@echo 'CAMLP5LIB = $(CAMLP5LIB)'
+	@echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)'
+	@echo 'HASNATDYNLINK = $(HASNATDYNLINK)'
+	@echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)'
+	@echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)'
+	@echo 'OCAMLFIND = $(OCAMLFIND)'
+	@echo 'PP = $(PP)'
+	@echo 'COQFLAGS = $(COQFLAGS)'
+	@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
+	@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
+.PHONY:	printenv
+
+# Generate a .merlin file.  If you need to append directives to this
+# file you can extend the merlin-hook target in Makefile.local
+.merlin:
+	$(SHOW)'FILL .merlin'
+	$(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin
+	$(HIDE)echo 'B $(COQLIB)' >> .merlin
+	$(HIDE)echo 'S $(COQLIB)' >> .merlin
+	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
+		echo 'B $(COQLIB)$(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
+		echo 'S $(COQLIB)$(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;)
+	$(HIDE)$(MAKE) merlin-hook -f "$(SELF)"
+.PHONY: merlin
+
+merlin-hook::
+	@# Extension point
+.PHONY: merlin-hook
+
+# prints all variables
+debug:
+	$(foreach v,\
+		$(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\
+	       		$(.VARIABLES))),\
+	       	$(info $(v) = $($(v))))
+.PHONY: debug
+
+.DEFAULT_GOAL := all
diff --git a/extraction/_CoqProject b/extraction/_CoqProject
new file mode 100644
index 000000000..6b139342f
--- /dev/null
+++ b/extraction/_CoqProject
@@ -0,0 +1,11 @@
+-R theories TemplateExtraction
+-Q ../template-coq/theories Template
+-I ../template-coq/src
+
+theories/Ast.v
+theories/Induction.v
+theories/LiftSubst.v
+theories/UnivSubst.v
+theories/WcbvEval.v
+theories/Typing.v
+theories/Extract.v
diff --git a/extraction/theories/Ast.v b/extraction/theories/Ast.v
new file mode 100644
index 000000000..a98da59f6
--- /dev/null
+++ b/extraction/theories/Ast.v
@@ -0,0 +1,216 @@
+(* Distributed under the terms of the MIT license.   *)
+
+Require Import Coq.Strings.String.
+Require Import Coq.PArith.BinPos.
+Require Import List. Import ListNotations.
+From Template Require Import monad_utils.
+From Template Require Export univ uGraph Ast.
+
+(** Extracted terms
+
+  These are the terms produced by extraction:
+  compared to kernel terms, all proofs are translated to [tBox] and
+  casts are removed.
+*)
+
+Inductive term : Set :=
+| tBox       : term (* Represents all proofs *)
+| tRel       : nat -> term
+| tVar       : ident -> term (* For free variables (e.g. in a goal) *)
+| tMeta      : nat -> term   (* NOTE: this will go away *)
+| tEvar      : nat -> list term -> term
+| tSort      : universe -> term
+| tProd      : name -> term (* the type *) -> term -> term
+| tLambda    : name -> term -> term -> term
+| tLetIn     : name -> term (* the term *) -> term -> term -> term
+| tApp       : term -> list term -> term
+| tConst     : kername -> universe_instance -> term
+| tInd       : inductive -> universe_instance -> term
+| tConstruct : inductive -> nat -> universe_instance -> term
+| tCase      : (inductive * nat) (* # of parameters *) -> term (* type info *)
+               -> term (* discriminee *) -> list (nat * term) (* branches *) -> term
+| tProj      : projection -> term -> term
+| tFix       : mfixpoint term -> nat -> term
+| tCoFix     : mfixpoint term -> nat -> term.
+
+
+
+Definition mkApps t us :=
+  match us with
+  | nil => t
+  | _ => match t with
+        | tApp f args => tApp f (args ++ us)
+        | _ => tApp t us
+        end
+  end.
+
+Definition mkApp t u := Eval cbn in mkApps t [u].
+
+Definition isApp t :=
+  match t with
+  | tApp _ _ => true
+  | _ => false
+  end.
+
+(** Well-formed terms: invariants which are not ensured by the OCaml type system *)
+
+Inductive wf : term -> Prop :=
+| wf_tBox : wf tBox
+| wf_tRel n : wf (tRel n)
+| wf_tVar id : wf (tVar id)
+| wf_tMeta n : wf (tMeta n)
+| wf_tEvar n l : Forall wf l -> wf (tEvar n l)
+| wf_tSort u : wf (tSort u)
+| wf_tProd na t b : wf t -> wf b -> wf (tProd na t b)
+| wf_tLambda na t b : wf t -> wf b -> wf (tLambda na t b)
+| wf_tLetIn na t b b' : wf t -> wf b -> wf b' -> wf (tLetIn na t b b')
+| wf_tApp t u : ~ isApp t = true -> u <> nil -> wf t -> Forall wf u -> wf (tApp t u)
+| wf_tConst k u : wf (tConst k u)
+| wf_tInd i u : wf (tInd i u)
+| wf_tConstruct i k u : wf (tConstruct i k u)
+| wf_tCase ci p c brs : wf p -> wf c -> Forall (Program.Basics.compose wf snd) brs -> wf (tCase ci p c brs)
+| wf_tProj p t : wf t -> wf (tProj p t)
+| wf_tFix mfix k : Forall (fun def => wf def.(dtype _) /\ wf def.(dbody _)) mfix -> wf (tFix mfix k)
+| wf_tCoFix mfix k : Forall (fun def => wf def.(dtype _) /\ wf def.(dbody _)) mfix -> wf (tCoFix mfix k).
+
+(** ** Entries
+
+  The kernel accepts these inputs and typechecks them to produce
+  declarations. Reflects [kernel/entries.mli].
+*)
+
+(** *** Constant and axiom entries *)
+
+Record parameter_entry := {
+  parameter_entry_type      : term;
+  parameter_entry_universes : universe_context }.
+
+Record definition_entry := {
+  definition_entry_type      : term;
+  definition_entry_body      : term;
+  definition_entry_universes : universe_context;
+  definition_entry_opaque    : bool }.
+
+
+Inductive constant_entry :=
+| ParameterEntry  (p : parameter_entry)
+| DefinitionEntry (def : definition_entry).
+
+(** *** Inductive entries *)
+
+(** This is the representation of mutual inductives.
+    nearly copied from [kernel/entries.mli]
+
+  Assume the following definition in concrete syntax:
+
+[[
+  Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1
+  ...
+  with      Ip (x1:X1) ... (xn:Xn) : Ap := cp1 : Tp1  ... | cpnp : Tpnp.
+]]
+
+  then, in [i]th block, [mind_entry_params] is [xn:Xn;...;x1:X1];
+  [mind_entry_arity] is [Ai], defined in context [x1:X1;...;xn:Xn];
+  [mind_entry_lc] is [Ti1;...;Tini], defined in context
+  [A'1;...;A'p;x1:X1;...;xn:Xn] where [A'i] is [Ai] generalized over
+  [x1:X1;...;xn:Xn].
+*)
+
+Inductive recursivity_kind :=
+  | Finite (* = inductive *)
+  | CoFinite (* = coinductive *)
+  | BiFinite (* = non-recursive, like in "Record" definitions *).
+
+Inductive local_entry : Set :=
+| LocalDef : term -> local_entry (* local let binding *)
+| LocalAssum : term -> local_entry.
+
+Record one_inductive_entry : Set := {
+  mind_entry_typename : ident;
+  mind_entry_arity : term;
+  mind_entry_template : bool; (* template polymorphism *)
+  mind_entry_consnames : list ident;
+  mind_entry_lc : list term (* constructor list *) }.
+
+Record mutual_inductive_entry := {
+  mind_entry_record    : option (option ident);
+  (* Is this mutual inductive defined as a record?
+     If so, is it primitive, using binder name [ident]
+     for the record in primitive projections ? *)
+  mind_entry_finite    : recursivity_kind;
+  mind_entry_params    : list (ident * local_entry);
+  mind_entry_inds      : list one_inductive_entry;
+  mind_entry_universes : universe_context;
+  mind_entry_private   : option bool
+  (* Private flag for sealing an inductive definition in an enclosing
+     module. Not handled by Template Coq yet. *) }.
+
+
+
+(** ** Declarations *)
+
+(** *** The context of De Bruijn indices *)
+
+Record context_decl := {
+  decl_name : name ;
+  decl_body : option term ;
+  decl_type : term }.
+
+(** Local (de Bruijn) variable binding *)
+
+Definition vass x A := {| decl_name := x; decl_body := None; decl_type := A |}.
+
+(** Local (de Bruijn) let-binding *)
+
+Definition vdef x t A := {| decl_name := x; decl_body := Some t; decl_type := A |}.
+
+(** Local (de Bruijn) context *)
+
+Definition context := list context_decl.
+
+(** Last declaration first *)
+
+Definition snoc {A} (Γ : list A) (d : A) := d :: Γ.
+
+Notation " Γ ,, d " := (snoc Γ d) (at level 20, d at next level).
+
+(** *** Environments *)
+
+(** See [one_inductive_body] from [declarations.ml]. *)
+Record one_inductive_body : Set := {
+  ind_name : ident;
+  ind_type : term; (* Closed arity *)
+  ind_kelim : list sort_family; (* Allowed elimination sorts *)
+  ind_ctors : list (ident * term (* Under context of arities of the mutual inductive *)
+                    * nat (* arity, w/o lets, w/o parameters *));
+  ind_projs : list (ident * term) (* names and types of projections, if any.
+                                     Type under context of params and inductive object *) }.
+
+(** See [mutual_inductive_body] from [declarations.ml]. *)
+Record mutual_inductive_body := {
+  ind_npars : nat;
+  ind_bodies : list one_inductive_body ;
+  ind_universes : universe_context }.
+
+(** See [constant_body] from [declarations.ml] *)
+Record constant_body := {
+    cst_type : term;
+    cst_body : option term;
+    cst_universes : universe_context }.
+
+Inductive global_decl :=
+| ConstantDecl : kername -> constant_body -> global_decl
+| InductiveDecl : kername -> mutual_inductive_body -> global_decl.
+
+Definition global_declarations := list global_decl.
+
+(** A context of global declarations + global universe constraints,
+    i.e. a global environment *)
+
+Definition global_context : Type := global_declarations * uGraph.t.
+
+(** *** Programs
+
+  A set of declarations and a term, as produced by [Quote Recursively]. *)
+
+Definition program : Type := global_declarations * term.
diff --git a/extraction/theories/Extract.v b/extraction/theories/Extract.v
new file mode 100644
index 000000000..f62f18ba9
--- /dev/null
+++ b/extraction/theories/Extract.v
@@ -0,0 +1,320 @@
+(* Distributed under the terms of the MIT license.   *)
+
+From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
+From Template Require Import config utils monad_utils Ast univ Induction LiftSubst UnivSubst Typing Checker Retyping MetaTheory WcbvEval.
+From TemplateExtraction Require Ast Typing WcbvEval.
+Require Import String.
+Local Open Scope string_scope.
+Set Asymmetric Patterns.
+Import MonadNotation.
+
+Existing Instance config.default_checker_flags.
+
+Definition is_prop_sort s :=
+  match Universe.level s with
+  | Some l => Level.is_prop l
+  | None => false
+  end.
+
+Module E := TemplateExtraction.Ast.
+
+Section Erase.
+  Context `{F : Fuel}.
+  Context (Σ : global_context).
+
+  Definition is_box c :=
+    match c with
+    | E.tBox => true
+    | _ => false
+    end.
+
+  Definition on_snd_map {A B C} (f : B -> C) (p : A * B) :=
+    (fst p, f (snd p)).
+
+  Section EraseMfix.
+    Context (extract : forall (Γ : context) (t : term), typing_result E.term).
+
+    Definition extract_mfix Γ (defs : mfixpoint term) :=
+      let Γ' := (fix_decls defs ++ Γ)%list in
+      monad_map (fun d => dtype' <- extract Γ d.(dtype);;
+                        dbody' <- extract Γ' d.(dbody);;
+                        ret ({| dname := d.(dname); rarg := d.(rarg);
+                                dtype := dtype'; dbody := dbody' |})) defs.
+  End EraseMfix.
+  
+  Fixpoint extract (Γ : context) (t : term) : typing_result E.term :=
+    s <- sort_of Σ Γ t;;
+    if is_prop_sort s then ret E.tBox
+    else match t with
+    | tRel i => ret (E.tRel i)
+    | tVar n => ret (E.tVar n)
+    | tMeta m => ret (E.tMeta m)
+    | tEvar m l =>
+      l' <- monad_map (extract Γ) l;;
+      ret (E.tEvar m l')
+    | tSort u => ret (E.tSort u)
+    | tConst kn u => ret (E.tConst kn u)
+    | tInd kn u => ret (E.tInd kn u)
+    | tConstruct kn k u => ret (E.tConstruct kn k u)
+    | tCast t k ty => extract Γ t
+                      (* ty' <- extract Γ ty ;; *)
+                      (* ret (tCast t' k ty') *)
+    | tProd na b t => b' <- extract Γ b;;
+                      t' <- extract (vass na b :: Γ) t;;
+                      ret (E.tProd na b' t')
+    | tLambda na b t =>
+      b' <- extract Γ b;;
+      t' <- extract (vass na b :: Γ) t;;
+      ret (E.tLambda na b' t')
+    | tLetIn na b t0 t1 =>
+      b' <- extract Γ b;;
+      t0' <- extract Γ t0;;
+      t1' <- extract (vdef na b t0 :: Γ) t1;;
+      ret (E.tLetIn na b' t0' t1')
+    | tApp f l =>
+      f' <- extract Γ f;;
+      l' <- monad_map (extract Γ) l;;
+      ret (E.tApp f' l') (* if is_dummy f' then ret dummy else *)
+    | tCase ip p c brs =>
+      c' <- extract Γ c;;
+      if is_box c' then
+        match brs with
+        | (_, x) :: _ => extract Γ x (* Singleton elimination *)
+        | nil =>
+          p' <- extract Γ p;;
+          ret (E.tCase ip p' c' nil) (* Falsity elimination *)
+        end
+      else
+        brs' <- monad_map (T:=typing_result) (fun x => x' <- extract Γ (snd x);; ret (fst x, x')) brs;;
+        p' <- extract Γ p;;
+        ret (E.tCase ip p' c' brs')
+    | tProj p c =>
+      c' <- extract Γ c;;
+      ret (E.tProj p c')
+    | tFix mfix n =>
+      mfix' <- extract_mfix extract Γ mfix;;
+      ret (E.tFix mfix' n)
+    | tCoFix mfix n =>
+      mfix' <- extract_mfix extract Γ mfix;;
+      ret (E.tCoFix mfix' n)
+     end.
+
+End Erase.
+
+Definition optM {M : Type -> Type} `{Monad M} {A B} (x : option A) (f : A -> M B) : M (option B) :=
+  match x with
+  | Some x => y <- f x ;; ret (Some y)
+  | None => ret None
+  end.
+
+Definition extract_constant_body `{F:Fuel} Σ (cb : constant_body) : typing_result E.constant_body :=
+  ty <- extract Σ [] cb.(cst_type) ;;
+  body <- optM cb.(cst_body) (fun b => extract Σ [] b);;
+  ret {| E.cst_universes := cb.(cst_universes);
+         E.cst_type := ty; E.cst_body := body; |}.
+
+Definition extract_one_inductive_body `{F:Fuel} Σ
+           (oib : one_inductive_body) : typing_result E.one_inductive_body :=
+  type <- extract Σ [] oib.(ind_type) ;;
+  ctors <- monad_map (fun '(x, y, z) => y' <- extract Σ [] y;; ret (x, y', z)) oib.(ind_ctors);;
+  projs <- monad_map (fun '(x, y) => y' <- extract Σ [] y;; ret (x, y')) oib.(ind_projs);;
+  ret {| E.ind_name := oib.(ind_name);
+         E.ind_type := type;
+         E.ind_kelim := oib.(ind_kelim);
+         E.ind_ctors := ctors;
+         E.ind_projs := projs |}.
+
+Definition extract_mutual_inductive_body `{F:Fuel} Σ
+           (mib : mutual_inductive_body) : typing_result E.mutual_inductive_body :=
+  bodies <- monad_map (extract_one_inductive_body Σ) mib.(ind_bodies) ;;
+  ret {| E.ind_npars := mib.(ind_npars);
+         E.ind_bodies := bodies;
+         E.ind_universes := mib.(ind_universes) |}.
+
+Fixpoint extract_global_decls univs Σ : typing_result E.global_declarations :=
+  match Σ with
+  | [] => ret []
+  | ConstantDecl kn cb :: Σ =>
+    cb' <- extract_constant_body (Σ, univs) cb;;
+    Σ' <- extract_global_decls univs Σ;;
+    ret (E.ConstantDecl kn cb' :: Σ')
+  | InductiveDecl kn mib :: Σ =>
+    mib' <- extract_mutual_inductive_body (Σ, univs) mib;;
+    Σ' <- extract_global_decls univs Σ;;
+    ret (E.InductiveDecl kn mib' :: Σ')
+  end.
+
+Definition extract_global Σ :=
+  let '(Σ, univs) := Σ in
+  Σ' <- extract_global_decls univs Σ;;
+  ret (Σ', univs).
+
+(** * Erasure correctness
+    
+    The statement below expresses that any well-typed term's
+    extraction has the same operational semantics as its source, under
+    a few conditions:
+
+    - The terms has to be locally closed, otherwise evaluation could get 
+      stuck on free variables. Typing under an empty context ensures that.
+    - The global environment is axiom-free, for the same reason.
+    - The object is of inductive type, or more generally a function resulting 
+      ultimately in an inductive value when applied.
+
+   We use an observational equality relation to relate the two values, 
+   which is indifferent to the extractd parts.
+ *)
+
+Fixpoint inductive_arity (t : term) :=
+  match t with
+  | tApp f _ | f =>
+    match f with
+    | tInd ind u => Some ind
+    | _ => None
+    end
+  end.
+
+(* Inductive inductive_arity : term -> Prop := *)
+(* | inductive_arity_concl ind u args : inductive_arity (mkApps (tInd ind u) args) *)
+(* | inductive_arity_arrow na b t : inductive_arity t -> inductive_arity (tProd na b t). *)
+
+Definition option_is_none {A} (o : option A) :=
+  match o with
+  | Some _ => false
+  | None => true
+  end.
+
+Definition is_axiom_decl g :=
+  match g with
+  | ConstantDecl kn cb => option_is_none cb.(cst_body)
+  | InductiveDecl kn ind => false
+  end.
+
+Definition axiom_free Σ :=
+  List.forallb (fun g => negb (is_axiom_decl g)) Σ.
+
+Definition computational_ind Σ ind :=
+  let 'mkInd mind n := ind in
+  let mib := lookup_env Σ mind in
+  match mib with
+  | Some (InductiveDecl kn decl) =>
+    match List.nth_error decl.(ind_bodies) n with
+    | Some body =>
+      match destArity [] body.(ind_type) with
+      | Some arity => negb (is_prop_sort (snd arity))
+      | None => false
+      end
+    | None => false
+    end
+  | _ => false
+  end.
+
+Require Import Bool.
+Coercion is_true : bool >-> Sortclass.
+
+Definition computational_type Σ T :=
+  exists ind, inductive_arity T = Some ind /\ computational_ind Σ ind.
+
+(** The precondition on the extraction theorem. *)
+
+Record extraction_pre (Σ : global_context) t T :=
+  { extr_typed : Σ ;;; [] |- t : T;
+    extr_env_axiom_free : axiom_free (fst Σ);
+    extr_computational_type : computational_type Σ T }.
+
+(** The observational equivalence relation between source and extractd values. *)
+
+Definition destApp t :=
+  match t with
+  | tApp f args => (f, args)
+  | f => (f, [])
+  end.
+
+Inductive Question : Set  := 
+| Cnstr : Ast.inductive -> nat -> Question 
+| Abs : Question.
+
+Definition observe (q : Question) (v : E.term) : bool :=
+  match q with
+  | Cnstr i k =>
+    match v with
+    | E.tConstruct i' k' u =>
+      eq_ind i i' && eq_nat k k'
+    | _ => false
+    end
+  | Abs =>
+    match v with
+    | E.tLambda _ _ _ => true
+    | E.tFix _ _ => true
+    | _ => false
+    end
+  end.
+             
+
+(*
+Fixpoint obs_eq (Σ : global_context) (v v' : term) (T : term) (s : universe) : Prop :=
+  if is_prop_sort s then is_dummy v'
+  else
+    match T with
+    | tInd ind u =>
+      (* Canonical inductive value *)
+      let '(hd, args) := destApp v in
+      let '(hd', args') := destApp v' in
+      eq_term Σ hd hd' /\ obs_eq 
+      
+ | obs_eq_prf v T s : Σ ;;; [] |- v : T ->
+  Σ ;;; [] |- T : tSort s ->
+  is_prop_sort s ->
+  obs_eq Σ v dummy
+
+| obs_eq_cstr ind k u args args' T : Σ ;;; [] |- mkApps (tConstruct ind k u) args : T ->
+  computational_type Σ T ->
+  Forall2 (obs_eq Σ) args args' ->
+  obs_eq Σ (mkApps (tConstruct ind k u) args) (mkApps (tConstruct ind k u) args')
+
+| obs_eq_arrow na f f' T T' :
+    Σ ;;; [] |- f : tProd na T T' ->
+    (forall arg arg', obs_eq Σ arg arg' -> 
+    
+    obs_eq Σ f f'.                                     
+*)                      
+
+Record extraction_post (Σ : global_context) (Σ' : Ast.global_context) (t : term) (t' : E.term) :=
+  { extr_value : E.term;
+    extr_eval : TemplateExtraction.WcbvEval.eval (fst Σ') [] t' extr_value;
+    (* extr_equiv : obs_eq Σ v extr_value *) }.
+
+(** The extraction correctness theorem we conjecture. *)
+
+Definition erasure_correctness :=
+  forall Σ t T, extraction_pre Σ t T ->
+  forall v, eval Σ [] t v ->
+  forall (f : Fuel) Σ' (t' : E.term),
+    extract Σ [] t = Checked t' ->
+    extract_global Σ = Checked Σ' ->
+    extraction_post Σ Σ' t t'.
+      
+Conjecture erasure_correct : erasure_correctness.
+
+Quote Recursively Definition zero_syntax := 0.
+
+Definition extract_rec (t : global_declarations * term) : typing_result E.term :=
+  let '(Σ, t) := t in
+  extract (reconstruct_global_context Σ) [] t.
+
+(* A few tests *)
+
+Quote Recursively Definition true_syntax := I.
+Eval vm_compute in extract_rec true_syntax.
+
+Quote Recursively Definition exist_syntax := (exist _ 0 I : { x : nat | True }).
+Eval vm_compute in extract_rec exist_syntax.
+
+Quote Recursively Definition exist'_syntax := ((exist _ (S 0) (le_n (S 0))) : { x : nat | 0 < x }).
+Eval vm_compute in extract_rec exist'_syntax.
+
+Quote Recursively Definition fun_syntax := (fun (x : nat) (bla : x < 0) => x).
+Eval vm_compute in extract_rec fun_syntax. (* Not erasing bindings *)
+
+Quote Recursively Definition fun'_syntax := (fun (x : nat) (bla : x < 0) => bla).
+Eval vm_compute in extract_rec fun'_syntax.
diff --git a/extraction/theories/Induction.v b/extraction/theories/Induction.v
new file mode 100644
index 000000000..39110cab2
--- /dev/null
+++ b/extraction/theories/Induction.v
@@ -0,0 +1,354 @@
+(* Distributed under the terms of the MIT license.   *)
+
+From Template Require Import univ.
+From TemplateExtraction Require Import Ast.
+Require Import List Program.
+Require Import BinPos.
+Require Import Coq.Arith.Compare_dec Bool.
+Set Asymmetric Patterns.
+
+(** * Deriving a compact induction principle for terms
+
+  *WIP*
+
+  Allows to get the right induction principle on lists of terms appearing
+  in the term syntax (in evar, applications, branches of cases and (co-)fixpoints. *)
+
+Arguments dname {term} _.
+Arguments dtype {term} _.
+Arguments dbody {term} _.
+Arguments rarg {term} _.
+
+Definition on_snd {A B} (f : B -> B) (p : A * B) :=
+  (fst p, f (snd p)).
+
+Definition map_def {term : Set} (f : term -> term) (d : def term) :=
+  {| dname := d.(dname); dtype := f d.(dtype); dbody := f d.(dbody); rarg := d.(rarg) |}.
+
+Definition test_snd {A B} (f : B -> bool) (p : A * B) :=
+  f (snd p).
+
+Definition test_def {term : Set} (f : term -> bool) (d : def term) :=
+  f d.(dtype) && f d.(dbody).
+
+Lemma on_snd_on_snd {A B} (f g : B -> B) (d : A * B) :
+  on_snd f (on_snd g d) = on_snd (fun x => f (g x)) d.
+Proof.
+  destruct d; reflexivity.
+Qed.
+
+Lemma compose_on_snd {A B} (f g : B -> B) :
+  compose (A:=A * B) (on_snd f) (on_snd g) = on_snd (compose f g).
+Proof.
+  reflexivity.
+Qed.
+
+
+Lemma map_def_map_def {term : Set} (f g : term -> term) (d : def term) :
+  map_def f (map_def g d) = map_def (fun x => f (g x)) d.
+Proof.
+  destruct d; reflexivity.
+Qed.
+
+Lemma compose_map_def {term : Set} (f g : term -> term) :
+  compose (A:=def term) (map_def f) (map_def g) = map_def (compose f g).
+Proof. reflexivity. Qed.
+
+Lemma combine_map_id {A B} (l : list (A * B)) :
+ l = combine (map fst l) (map snd l).
+Proof.
+  induction l ; simpl; try easy.
+  destruct a. now f_equal.
+Qed.
+
+Lemma map_map_compose :
+  forall (A B C : Type) (f : A -> B) (g : B -> C) (l : list A),
+    map g (map f l) = map (compose g f) l.
+Proof. apply map_map. Qed.
+Hint Unfold compose : terms.
+
+Lemma map_id_f {A} (l : list A) (f : A -> A) :
+  (forall x, f x = x) ->
+  map f l = l.
+Proof.
+  induction l; intros; simpl; try easy.
+  rewrite H. f_equal. eauto.
+Qed.
+
+Lemma map_def_id {t : Set} : map_def (@id t) = id.
+Proof. extensionality p. now destruct p. Qed.
+Hint Rewrite @map_def_id @map_id.
+
+(** Custom induction principle on syntax, dealing with the various lists appearing in terms. *)
+
+Definition tCaseBrsProp (P : term -> Prop) (l : list (nat * term)) :=
+  Forall (fun x => P (snd x)) l.
+
+Definition tFixProp (P : term -> Prop) (m : mfixpoint term) :=
+  Forall (fun x : def term => P x.(dtype) /\ P x.(dbody)) m.
+
+Lemma term_forall_list_ind :
+  forall P : term -> Prop,
+    (P tBox) ->
+    (forall n : nat, P (tRel n)) ->
+    (forall i : ident, P (tVar i)) ->
+    (forall n : nat, P (tMeta n)) ->
+    (forall (n : nat) (l : list term), Forall P l -> P (tEvar n l)) ->
+    (forall s, P (tSort s)) ->
+    (forall (n : name) (t : term), P t -> forall t0 : term, P t0 -> P (tProd n t t0)) ->
+    (forall (n : name) (t : term), P t -> forall t0 : term, P t0 -> P (tLambda n t t0)) ->
+    (forall (n : name) (t : term),
+        P t -> forall t0 : term, P t0 -> forall t1 : term, P t1 -> P (tLetIn n t t0 t1)) ->
+    (forall t : term, P t -> forall l : list term, Forall P l -> P (tApp t l)) ->
+    (forall (s : String.string) (u : list Level.t), P (tConst s u)) ->
+    (forall (i : inductive) (u : list Level.t), P (tInd i u)) ->
+    (forall (i : inductive) (n : nat) (u : list Level.t), P (tConstruct i n u)) ->
+    (forall (p : inductive * nat) (t : term),
+        P t -> forall t0 : term, P t0 -> forall l : list (nat * term),
+            tCaseBrsProp P l -> P (tCase p t t0 l)) ->
+    (forall (s : projection) (t : term), P t -> P (tProj s t)) ->
+    (forall (m : mfixpoint term) (n : nat), tFixProp P m -> P (tFix m n)) ->
+    (forall (m : mfixpoint term) (n : nat), tFixProp P m -> P (tCoFix m n)) ->
+    forall t : term, P t.
+Proof.
+  intros until t. revert t.
+  fix auxt 1.
+  move auxt at top. 
+  destruct t; match goal with
+                 H : _ |- _ => apply H
+              end; auto.
+  revert l.
+  fix auxl' 1.
+  destruct l; constructor; [|apply auxl'].
+  apply auxt.
+  revert l.
+  fix auxl' 1.
+  destruct l; constructor; [|apply auxl'].
+  apply auxt.
+  revert l.
+  fix auxl' 1.
+  destruct l; constructor; [|apply auxl'].
+  apply auxt.
+
+  revert m.
+  fix auxm 1.
+  destruct m; constructor; [|apply auxm].
+  split; apply auxt.
+  revert m.
+  fix auxm 1.
+  destruct m; constructor; [|apply auxm].
+  split; apply auxt.
+Defined.
+
+Lemma forall_map_spec {A} {P : A -> Prop} {l} {f g : A -> A} :
+  Forall P l -> (forall x, P x -> f x = g x) ->
+  map f l = map g l.
+Proof.
+  induction 1; simpl; trivial.
+  intros Heq. rewrite Heq. f_equal. apply IHForall. apply Heq. apply H.
+Qed.
+
+Lemma on_snd_spec {A B} (P : B -> Prop) (f g : B -> B) (x : A * B) :
+  P (snd x) -> (forall x, P x -> f x = g x) ->
+  on_snd f x = on_snd g x.
+Proof.
+  intros. destruct x. unfold on_snd. simpl.
+  now rewrite H0; auto.
+Qed.
+
+Lemma map_def_spec (P : term -> Prop) (f g : term -> term) (x : def term) :
+  P x.(dbody) -> P x.(dtype) -> (forall x, P x -> f x = g x) ->
+  map_def f x = map_def g x.
+Proof.
+  intros. destruct x. unfold map_def. simpl.
+  rewrite !H1; auto. 
+Qed.
+
+Lemma case_brs_map_spec {P : term -> Prop} {l} {f g : term -> term} :
+  tCaseBrsProp P l -> (forall x, P x -> f x = g x) ->
+  map (on_snd f) l = map (on_snd g) l.
+Proof.
+  intros.
+  eapply (forall_map_spec H).
+  intros.
+  eapply on_snd_spec; eauto.
+Qed.
+
+Lemma tfix_map_spec {P : term -> Prop} {l} {f g : term -> term} :
+  tFixProp P l -> (forall x, P x -> f x = g x) ->
+  map (map_def f) l = map (map_def g) l.
+Proof.
+  intros.
+  eapply (forall_map_spec H).
+  intros. destruct H1;
+  eapply map_def_spec; eauto.
+Qed.
+
+
+Lemma forall_forallb_map_spec {A : Type} {P : A -> Prop} {p : A -> bool}
+      {l : list A} {f g : A -> A} :
+    Forall P l -> forallb p l = true ->
+    (forall x : A, P x -> p x = true -> f x = g x) -> map f l = map g l.
+Proof.
+  induction 1; simpl; trivial.
+  rewrite andb_true_iff. intros [px pl] Hx.
+  f_equal. now apply Hx. now apply IHForall. 
+Qed.
+
+Lemma on_snd_test_spec {A B} (P : B -> Prop) (p : B -> bool) (f g : B -> B) (x : A * B) :
+  P (snd x) -> (forall x, P x -> p x = true -> f x = g x) ->
+  test_snd p x = true ->
+  on_snd f x = on_snd g x.
+Proof.
+  intros. destruct x. unfold on_snd. simpl.
+  now rewrite H0; auto.
+Qed.
+
+Lemma map_def_test_spec (P : term -> Prop) p (f g : term -> term) (x : def term) :
+  P x.(dbody) -> P x.(dtype) -> (forall x, P x -> p x = true -> f x = g x) ->
+  test_def p x = true ->
+  map_def f x = map_def g x.
+Proof.
+  intros. destruct x. unfold map_def. simpl.
+  unfold test_def in H2; simpl in H2. rewrite andb_true_iff in H2.
+  rewrite !H1; intuition auto. 
+Qed.
+
+Lemma case_brs_forallb_map_spec {P : term -> Prop} {p : term -> bool}
+      {l} {f g : term -> term} :
+  tCaseBrsProp P l -> 
+  forallb (test_snd p) l = true ->
+  (forall x, P x -> p x = true -> f x = g x) ->
+  map (on_snd f) l = map (on_snd g) l.
+Proof.
+  intros.
+  eapply (forall_forallb_map_spec H H0).
+  intros.
+  eapply on_snd_test_spec; eauto.
+Qed.
+
+Lemma tfix_forallb_map_spec {P : term -> Prop} {p} {l} {f g : term -> term} :
+  tFixProp P l -> 
+  forallb (test_def p) l = true ->
+  (forall x, P x -> p x = true -> f x = g x) ->
+  map (map_def f) l = map (map_def g) l.
+Proof.
+  intros.
+  eapply (forall_forallb_map_spec H H0).
+  intros. destruct H2.
+  eapply map_def_test_spec; eauto.
+Qed.
+
+Ltac apply_spec :=
+  match goal with
+  | H : Forall _ _, H' : forallb _ _ = _ |- map _ _ = map _ _ =>
+    eapply (forall_forallb_map_spec H H')
+  | H : Forall _ _ |- map _ _ = map _ _ =>
+    eapply (forall_map_spec H)
+  | H : tCaseBrsProp _ _, H' : forallb _ _ = _ |- map _ _ = map _ _ =>
+    eapply (case_brs_forallb_map_spec H H')
+  | H : tCaseBrsProp _ _ |- map _ _ = map _ _ =>
+    eapply (case_brs_map_spec H)
+  | H : tFixProp _ _, H' : forallb _ _ = _ |- map _ _ = map _ _ =>
+    eapply (tfix_forallb_map_spec H H')
+  | H : tFixProp _ _ |- map _ _ = map _ _ =>
+    eapply (tfix_map_spec H)
+  end.
+
+Lemma lift_to_list (P : term -> Prop) : (forall t, wf t -> P t) -> forall l, Forall wf l -> Forall P l.
+Proof.
+  intros IH.
+  fix 1.
+  destruct l; constructor.
+  apply IH. now inversion_clear H.
+  apply lift_to_list. now inversion_clear H.
+Defined.
+
+Lemma lift_to_wf_list (P : term -> Prop) : forall l, Forall (fun t => wf t -> P t) l -> Forall wf l -> Forall P l.
+Proof.
+  induction 1. constructor.
+  inversion_clear 1. specialize (IHForall H3).
+  constructor; auto.
+Qed.
+
+Ltac applyhyp :=
+  match goal with
+    H : _ |- _ => apply H
+  end.
+
+Class Hyp (T : Type) := hyp : T.
+Hint Extern 10 (Hyp _) => exactly_once multimatch goal with H : _ |- _
+=> exact H end : typeclass_instances.
+Class AHyp (T : Type) := ahyp : T.
+Hint Extern 10 (AHyp _) => multimatch goal with H : _ |- _
+=> eapply H; shelve end : typeclass_instances.
+
+Ltac inv H :=
+  inversion_clear H ||
+  match H with
+  | @hyp _ ?X => inversion_clear X
+  | @ahyp _ ?X => inversion_clear X
+  end.
+
+
+Lemma term_wf_forall_list_ind :
+  forall P : term -> Prop,
+    (P tBox) ->
+    (forall n : nat, P (tRel n)) ->
+    (forall i : ident, P (tVar i)) ->
+    (forall n : nat, P (tMeta n)) ->
+    (forall (n : nat) (l : list term), Forall P l -> P (tEvar n l)) ->
+    (forall s, P (tSort s)) ->
+    (forall (n : name) (t : term), P t -> forall t0 : term, P t0 -> P (tProd n t t0)) ->
+    (forall (n : name) (t : term), P t -> forall t0 : term, P t0 -> P (tLambda n t t0)) ->
+    (forall (n : name) (t : term),
+        P t -> forall t0 : term, P t0 -> forall t1 : term, P t1 -> P (tLetIn n t t0 t1)) ->
+    (forall t : term, ~ isApp t = true -> P t -> forall l : list term, l <> nil -> Forall P l -> P (tApp t l)) ->
+    (forall (s : String.string) (u : list Level.t), P (tConst s u)) ->
+    (forall (i : inductive) (u : list Level.t), P (tInd i u)) ->
+    (forall (i : inductive) (n : nat) (u : list Level.t), P (tConstruct i n u)) ->
+    (forall (p : inductive * nat) (t : term),
+        P t -> forall t0 : term, P t0 -> forall l : list (nat * term),
+            tCaseBrsProp P l -> P (tCase p t t0 l)) ->
+    (forall (s : projection) (t : term), P t -> P (tProj s t)) ->
+    (forall (m : mfixpoint term) (n : nat), tFixProp P m -> P (tFix m n)) ->
+    (forall (m : mfixpoint term) (n : nat), tFixProp P m -> P (tCoFix m n)) ->
+    forall t : term, wf t -> P t.
+Proof.
+  intros P; intros until t. revert t.
+  apply (term_forall_list_ind (fun t => wf t -> P t));
+    intros; try solve [match goal with
+                 H : _ |- _ => apply H
+                       end; auto].
+  unshelve apply (ahyp: (P (tEvar _ _))).
+  inv H17.
+  auto using lift_to_wf_list.
+
+  inv (hyp: wf _); auto.
+  inv (hyp: wf _); auto.
+  inv (hyp: wf _); auto.
+  inv (hyp: wf _); auto.
+
+  applyhyp; auto using lift_to_wf_list.
+
+  inv (hyp: wf _). applyhyp; auto.
+  red.
+  red in H18.
+  induction H18.
+  constructor.
+  inv H22; auto.
+
+  inv H17; auto.
+
+  inv H17; auto.
+  apply H14. red.
+  red in H16.
+  induction H16. constructor.
+  inv H18; constructor; intuition auto.
+
+  inv H17; auto.
+  apply H15. red.
+  red in H16.
+  induction H16. constructor.
+  inv H18; constructor; intuition auto.
+Qed.
diff --git a/extraction/theories/LiftSubst.v b/extraction/theories/LiftSubst.v
new file mode 100644
index 000000000..385ebad1e
--- /dev/null
+++ b/extraction/theories/LiftSubst.v
@@ -0,0 +1,524 @@
+(* Distributed under the terms of the MIT license.   *)
+
+From Coq Require Import List Program BinPos Arith.Compare_dec Bool.
+From TemplateExtraction Require Import Ast Induction.
+
+(** * Lifting and substitution for the AST
+
+  Along with standard commutation lemmas.
+  Definition of [closedn] (boolean) predicate for checking if
+  a term is closed. *)
+
+Set Asymmetric Patterns.
+
+Fixpoint lift n k t : term :=
+  match t with
+  | tRel i => if Nat.leb k i then tRel (n + i) else tRel i
+  | tEvar ev args => tEvar ev (List.map (lift n k) args)
+  | tLambda na T M => tLambda na (lift n k T) (lift n (S k) M)
+  | tApp u v => tApp (lift n k u) (List.map (lift n k) v)
+  | tProd na A B => tProd na (lift n k A) (lift n (S k) B)
+  | tLetIn na b t b' => tLetIn na (lift n k b) (lift n k t) (lift n (S k) b')
+  | tCase ind p c brs =>
+    let brs' := List.map (on_snd (lift n k)) brs in
+    tCase ind (lift n k p) (lift n k c) brs'
+  | tProj p c => tProj p (lift n k c)
+  | tFix mfix idx =>
+    let k' := List.length mfix + k in
+    let mfix' := List.map (map_def (lift n k')) mfix in
+    tFix mfix' idx
+  | tCoFix mfix idx =>
+    let k' := List.length mfix + k in
+    let mfix' := List.map (map_def (lift n k')) mfix in
+    tCoFix mfix' idx
+  | x => x
+  end.
+
+
+Notation lift0 n := (lift n 0).
+Definition up := lift 1 0.
+
+Fixpoint subst t k u :=
+  match u with
+  | tRel n =>
+    match Nat.compare k n with
+    | Datatypes.Eq => lift0 k t
+    | Datatypes.Gt => tRel n
+    | Datatypes.Lt => tRel (pred n)
+    end
+  | tEvar ev args => tEvar ev (List.map (subst t k) args)
+  | tLambda na T M => tLambda na (subst t k T) (subst t (S k) M)
+  | tApp u v => mkApps (subst t k u) (List.map (subst t k) v)
+  | tProd na A B => tProd na (subst t k A) (subst t (S k) B)
+  | tLetIn na b ty b' => tLetIn na (subst t k b) (subst t k ty) (subst t (S k) b')
+  | tCase ind p c brs =>
+    let brs' := List.map (on_snd (subst t k)) brs in
+    tCase ind (subst t k p) (subst t k c) brs'
+  | tProj p c => tProj p (subst t k c)
+  | tFix mfix idx =>
+    let k' := List.length mfix + k in
+    let mfix' := List.map (map_def (subst t k')) mfix in
+    tFix mfix' idx
+  | tCoFix mfix idx =>
+    let k' := List.length mfix + k in
+    let mfix' := List.map (map_def (subst t k')) mfix in
+    tCoFix mfix' idx
+  | x => x
+  end.
+
+Notation subst0 t := (subst t 0).
+Notation "M { j := N }" := (subst N j M) (at level 10, right associativity).
+
+(** Substitutes [t1 ; .. ; tn] in u for [Rel 0; .. Rel (n-1)]*)
+Definition substl l t :=
+  List.fold_left (fun t u => subst0 u t) l t.
+
+Fixpoint closedn k (t : term) : bool :=
+  match t with
+  | tRel i => Nat.ltb i k
+  | tEvar ev args => List.forallb (closedn k) args
+  | tLambda _ T M | tProd _ T M => closedn k T && closedn (S k) M
+  | tApp u v => closedn k u && List.forallb (closedn k) v
+  | tLetIn na b t b' => closedn k b && closedn k t && closedn (S k) b'
+  | tCase ind p c brs =>
+    let brs' := List.forallb (test_snd (closedn k)) brs in
+    closedn k p && closedn k c && brs'
+  | tProj p c => closedn k c
+  | tFix mfix idx =>
+    let k' := List.length mfix + k in
+    List.forallb (test_def (closedn k')) mfix
+  | tCoFix mfix idx =>
+    let k' := List.length mfix + k in
+    List.forallb (test_def (closedn k')) mfix
+  | x => true
+  end.
+
+Notation closed t := (closedn 0 t).
+
+Create HintDb terms.
+
+Ltac easy0 :=
+  let rec use_hyp H :=
+   (match type of H with
+    | _ /\ _ => exact H || destruct_hyp H
+    | _ => try (solve [ inversion H ])
+    end)
+  with do_intro := (let H := fresh in
+                    intro H; use_hyp H)
+  with destruct_hyp H := (case H; clear H; do_intro; do_intro)
+  in
+  let rec use_hyps :=
+   (match goal with
+    | H:_ /\ _ |- _ => exact H || (destruct_hyp H; use_hyps)
+    | H:_ |- _ => solve [ inversion H ]
+    | _ => idtac
+    end)
+  in
+  let do_atom := (solve [ trivial with eq_true | reflexivity | symmetry; trivial | contradiction ]) in
+  let rec do_ccl := (try do_atom; repeat (do_intro; try do_atom); (solve [ split; do_ccl ])) in
+  (solve [ do_atom | use_hyps; do_ccl ]) || fail "Cannot solve this goal".
+Require Import Omega.
+Hint Extern 100 => omega : terms.
+
+Ltac easy ::= easy0 || solve [eauto 7 with core arith terms].
+
+Notation lift_rec n c k := (lift n k c) (only parsing).
+Notation subst_rec N M k := (subst N k M) (only parsing).
+
+Require Import PeanoNat.
+Import Nat.
+
+Lemma lift_rel_ge :
+  forall k n p, p <= n -> lift_rec k (tRel n) p = tRel (k + n).
+Proof.
+  intros; simpl in |- *.
+  now elim (leb_spec p n).
+Qed.
+
+Lemma lift_rel_lt : forall k n p, p > n -> lift_rec k (tRel n) p = tRel n.
+Proof.
+  intros; simpl in |- *.
+  now elim (leb_spec p n).
+Qed.
+
+Lemma lift_rel_alt : forall n k i, lift n k (tRel i) = tRel (if Nat.leb k i then n + i else i).
+Proof.
+  intros; simpl. now destruct leb.
+Qed.
+
+Lemma subst_rel_lt : forall u n k, k > n -> subst_rec u (tRel n) k = tRel n.
+Proof.
+  simpl in |- *; intros.
+  elim (compare_spec k n); intro Hcomp; easy.
+Qed.
+
+Lemma subst_rel_gt :
+  forall u n k, n > k -> subst_rec u (tRel n) k = tRel (pred n).
+Proof.
+  simpl in |- *; intros.
+  now elim (compare_spec k n). 
+Qed.
+
+Lemma subst_rel_eq : forall u n, subst_rec u (tRel n) n = lift0 n u.
+Proof.
+  intros; simpl in |- *.
+  now elim (compare_spec n n).
+Qed.
+
+Lemma lift_rec0 : forall M k, lift_rec 0 M k = M.
+Proof.
+  intros M.
+  elim M using term_forall_list_ind; simpl in |- *; intros; try easy ;
+    try (try rewrite H; try rewrite H0 ; try rewrite H1 ; easy).
+
+  - now elim (leb k n).
+  - f_equal. rewrite <- map_id. now eapply (forall_map_spec H).
+  - f_equal. auto. rewrite <- map_id. now eapply (forall_map_spec H0).
+  - f_equal; auto. rewrite <- map_id. eapply (forall_map_spec H1).
+    intros. destruct x; unfold on_snd. simpl. rewrite H2. reflexivity.
+
+  - f_equal. transitivity (map (map_def id) m). eapply (tfix_map_spec H); auto.
+    rewrite <- map_id. f_equal. extensionality x. destruct x; reflexivity.
+  - f_equal. transitivity (map (map_def id) m). eapply (tfix_map_spec H); auto.
+    rewrite <- map_id. f_equal. extensionality x. destruct x; reflexivity.
+Qed.
+
+Lemma lift0_p : forall M, lift0 0 M = M.
+  intros; unfold lift in |- *.
+  apply lift_rec0; easy.
+Qed.
+
+
+Lemma simpl_lift_rec :
+  forall M n k p i,
+    i <= k + n ->
+    k <= i -> lift_rec p (lift_rec n M k) i = lift_rec (p + n) M k.
+Proof.
+  intros M.
+  elim M using term_forall_list_ind;
+    intros; simpl; try easy;
+      rewrite ?map_map_compose, ?compose_on_snd, ?compose_map_def;
+      try (rewrite H, ?H0, ?H1; auto); try (f_equal; apply_spec);
+        try rewrite ?map_length; try easy.
+
+  - elim (leb_spec k n); intros.
+    now rewrite lift_rel_ge.
+    now rewrite lift_rel_lt.
+Qed.
+
+Lemma simpl_lift : forall M n, lift0 (S n) M = lift0 1 (lift0 n M).
+  now intros; rewrite simpl_lift_rec.
+Qed.
+
+Lemma permute_lift_rec :
+  forall M n k p i,
+    i <= k ->
+    lift_rec p (lift_rec n M k) i = lift_rec n (lift_rec p M i) (p + k).
+Proof.
+  intros M.
+  elim M using term_forall_list_ind;
+    intros; simpl; try easy;
+      rewrite ?map_map_compose, ?compose_on_snd, ?compose_map_def;
+      try solve [f_equal; easy];
+      try (f_equal; try easy; apply_spec);
+      unfold compose; intros;
+        try rewrite ?map_length; try easy ;
+        try (rewrite H, H0; f_equal; try easy; now f_equal);
+        try (rewrite H, H0, H1; f_equal; try easy; now f_equal);
+        try (rewrite H1; now f_equal).
+  
+  - elim (leb_spec k n); intros;
+    elim (leb_spec i n); intros; try easy.
+    + rewrite 2!lift_rel_ge; try easy.
+    + rewrite lift_rel_ge, lift_rel_lt; try easy.
+    + rewrite 2!lift_rel_lt; try easy.
+Qed.
+
+Lemma permute_lift :
+  forall M k, lift0 1 (lift_rec 1 M k) = lift_rec 1 (lift0 1 M) (S k).
+  intros.
+  change (lift_rec 1 (lift_rec 1 M k) 0 = lift_rec 1 (lift_rec 1 M 0) (1 + k))
+    in |- *.
+  apply permute_lift_rec; easy.
+Qed.
+
+Lemma Forall_map {A B} (P : B -> Prop) (f : A -> B) l : Forall (Program.Basics.compose P f) l -> Forall P (map f l).
+Proof.
+  induction 1; constructor; auto.
+Qed.
+
+Lemma Forall_impl {A} (P Q : A -> Prop) : forall l, Forall P l -> (forall x, P x -> Q x) -> Forall Q l.
+Proof.
+  induction 1; constructor; auto.
+Qed.
+
+Lemma lift_rec_isApp n k t : ~ isApp t = true -> ~ isApp (lift n k t) = true.
+Proof.
+  induction t; auto.
+  intros.
+  simpl. destruct leb; auto.
+Qed.
+
+Lemma map_non_nil {A B} (f : A -> B) l : l <> nil -> map f l <> nil.
+Proof.
+  intros. intro.
+  destruct l; try discriminate.
+  contradiction.
+Qed.
+
+Lemma lift_rec_wf n k t : wf t -> wf (lift_rec n t k).
+Proof.
+  intros wft; revert t wft k.
+  apply (term_wf_forall_list_ind (fun t => forall k, wf (lift n k t))) ; simpl; intros; try constructor; auto.
+  destruct leb; constructor.
+  apply Forall_map.
+  induction H; constructor; auto.
+  now apply lift_rec_isApp.
+  now apply map_non_nil.
+  apply Forall_map. eapply Forall_impl. apply H2. auto.
+  apply Forall_map. eapply Forall_impl. apply H1.
+  intros [n' t]. simpl. repeat red; simpl; auto.
+  apply Forall_map. eapply Forall_impl. apply H.
+  simpl. intros. red; intuition (simpl; auto).
+  apply Forall_map. eapply Forall_impl. apply H.
+  simpl. intros. red; intuition (simpl; auto).
+Qed.
+
+Lemma mkApps_tApp t l :
+  ~ isApp t = true -> l <> nil -> mkApps t l = tApp t l.
+Proof.
+  intros.
+  destruct l. simpl. contradiction.
+  destruct t; simpl; try reflexivity.
+  simpl in H. contradiction.
+Qed.
+
+Hint Unfold compose.
+Hint Transparent compose.
+
+Lemma simpl_subst_rec :
+  forall M (H : wf M) N n p k,
+    p <= n + k ->
+    k <= p -> subst_rec N (lift_rec (S n) M k) p = lift_rec n M k.
+Proof.
+  intros M wfM. induction wfM using term_wf_forall_list_ind;
+    intros; simpl; try easy;
+      rewrite ?map_map_compose, ?compose_on_snd, ?compose_map_def;
+      try solve [f_equal; easy];
+      try (f_equal; try easy; apply_spec); intros;
+        try rewrite ?map_length; try easy ||
+      (try rewrite H, H0; f_equal; try easy; now f_equal).
+  
+  - elim (leb_spec k n); intros; try easy.
+    + rewrite subst_rel_gt; try easy.
+    + rewrite subst_rel_lt; try easy.
+
+  - rewrite IHwfM; auto.
+    apply (lift_rec_isApp n k) in H.
+    rewrite mkApps_tApp; auto using map_non_nil.
+    f_equal. eapply forall_map_spec. apply H1; simpl; auto.
+    simpl; intros. typeclasses eauto with core.
+Qed.
+
+Lemma simpl_subst :
+  forall N M (H : wf M) n p, p <= n -> subst_rec N (lift0 (S n) M) p = lift0 n M.
+  intros; now apply simpl_subst_rec.
+Qed.
+
+Lemma mkApps_tRel n a l : mkApps (tRel n) (a :: l) = tApp (tRel n) (a :: l).
+Proof.
+  simpl. reflexivity.
+Qed.
+
+Lemma lift_mkApps n k t l : lift n k (mkApps t l) = mkApps (lift n k t) (map (lift n k) l).
+Proof.
+  revert n k t; induction l; intros n k t; destruct t; try reflexivity.
+  rewrite lift_rel_alt. rewrite !mkApps_tRel.
+  simpl lift.
+  simpl map. rewrite !mkApps_tRel.
+  f_equal. destruct leb; auto.
+
+  simpl. f_equal.
+  now rewrite map_app.
+Qed.
+
+Lemma commut_lift_subst_rec :
+  forall M N n p k,
+    k <= p ->
+    lift_rec n (subst_rec N M p) k = subst_rec N (lift_rec n M k) (n + p).
+Proof.
+  intros M.
+  elim M using term_forall_list_ind;
+    intros; simpl; try easy;
+      rewrite ?map_map_compose, ?compose_on_snd, ?compose_map_def;
+      try solve [f_equal; easy];
+      try (f_equal; try easy; apply_spec);
+      unfold compose; intros;
+        try rewrite ?map_length; try easy ;
+        try (rewrite H, H0; f_equal; try easy; now f_equal);
+        try (rewrite H, H0, H1; f_equal; try easy; now f_equal);
+        try (rewrite H1; now f_equal).
+  
+  - elim (compare_spec p n); elim (leb_spec k n); intros; subst; try easy.
+    + rewrite subst_rel_eq; try easy.
+      now rewrite simpl_lift_rec.
+    + rewrite subst_rel_gt; try easy.
+      now rewrite lift_rel_ge.
+    + rewrite lift_rel_ge; try easy.
+      now rewrite subst_rel_lt.
+    + rewrite lift_rel_lt; try easy.
+      now rewrite subst_rel_lt.
+
+  - rewrite lift_mkApps. f_equal. auto.
+    rewrite map_map_compose. apply_spec. intros.
+    now apply H2.
+Qed.
+
+Lemma commut_lift_subst :
+  forall M N k, subst_rec N (lift0 1 M) (S k) = lift0 1 (subst_rec N M k).
+  now intros; rewrite commut_lift_subst_rec.
+Qed.
+
+Lemma distr_lift_subst_rec :
+  forall M N n p k,
+    lift_rec n (subst_rec N M p) (p + k) =
+    subst_rec (lift_rec n N k) (lift_rec n M (S (p + k))) p.
+Proof.
+  intros M.
+  elim M using term_forall_list_ind;
+    intros; match goal with
+              |- context [tRel _] => idtac
+            | |- _ => simpl
+            end; try easy;
+      rewrite ?map_map_compose, ?compose_on_snd, ?compose_map_def;
+      try solve [f_equal; easy];
+      try (f_equal; try easy; apply_spec);
+      unfold compose; intros;
+        try rewrite ?map_length; try easy ;
+        try (erewrite H, <- H0; f_equal; try easy; now f_equal);
+        try (erewrite H, <- H0, <- H1; f_equal; try easy; now f_equal);
+        try (erewrite H1; now f_equal).
+  
+  - unfold subst at 1. unfold lift at 4.
+    elim (compare_spec p n); intros; try easy;
+    elim (leb_spec (S (p + k)) n); intros; subst; try easy.
+    
+    + rewrite subst_rel_eq. now rewrite <- permute_lift_rec. 
+    + rewrite lift_rel_ge; try easy.
+      now rewrite subst_rel_gt.
+    + rewrite lift_rel_lt; try easy.
+      now rewrite subst_rel_gt.
+    + rewrite lift_rel_lt; try easy.
+      now rewrite subst_rel_lt.
+
+  - rewrite lift_mkApps. f_equal; auto.
+    rewrite map_map_compose; apply_spec; simpl.
+    intros. apply H1.
+  - rewrite add_assoc, H0. f_equal. now f_equal.
+  - rewrite add_assoc, H0. f_equal. now f_equal.
+Qed.
+
+Lemma distr_lift_subst :
+  forall M N n k,
+    lift_rec n (subst0 N M) k = subst0 (lift_rec n N k) (lift_rec n M (S k)).
+Proof.
+  intros; unfold subst in |- *.
+  pattern k at 1 3 in |- *.
+  replace k with (0 + k); try easy.
+  apply distr_lift_subst_rec.
+Qed.
+
+Lemma mkApp_nested f l l' : mkApps (mkApps f l) l' = mkApps f (l ++ l').
+Proof.
+  induction l; destruct f; destruct l'; simpl; rewrite ?app_nil_r; auto.
+  f_equal. now rewrite <- app_assoc.
+Qed.
+
+Lemma subst_mkApps u k t l : subst u k (mkApps t l) = mkApps (subst u k t) (map (subst u k) l).
+Proof.
+  revert u k t; induction l; intros u k t; destruct t; try reflexivity.
+  intros. simpl mkApps at 1. simpl subst at 2. simpl subst at 1.
+  rewrite map_app. now rewrite mkApp_nested.
+Qed.
+
+Lemma distr_subst_rec :
+  forall M N (P : term) (wfP : wf P) n p,
+    subst_rec P (subst_rec N M p) (p + n) =
+    subst_rec (subst_rec P N n) (subst_rec P M (S (p + n))) p.
+Proof.
+  intros M.
+  elim M using term_forall_list_ind;
+    intros; match goal with
+              |- context [tRel _] => idtac
+            | |- _ => simpl
+            end; try easy;
+      rewrite ?map_map_compose, ?compose_on_snd, ?compose_map_def;
+      try solve [f_equal; easy];
+      try (f_equal; try easy; apply_spec);
+      unfold compose; intros;
+        try rewrite ?map_length; try easy ;
+        try (erewrite H, <- H0; f_equal; try easy; now f_equal);
+        try (erewrite H, <- H0, <- H1; f_equal; try easy; now f_equal);
+        try (erewrite H1; now f_equal).
+  
+  - unfold subst at 2. 
+    elim (compare_spec p n); intros; try easy.
+    
+    + subst. rewrite subst_rel_lt; try easy.
+      rewrite subst_rel_eq; try easy.
+      now rewrite <- commut_lift_subst_rec.
+    + unfold subst at 4.
+      elim (compare_spec (S (p + n0)) n); intros; subst; try easy.
+      ++ rewrite subst_rel_eq.
+         now rewrite simpl_subst_rec.
+      ++ rewrite !subst_rel_gt; try easy.
+      ++ rewrite subst_rel_lt; try easy.
+         now rewrite subst_rel_gt.
+    + rewrite !subst_rel_lt; try easy.
+
+  - rewrite !subst_mkApps. rewrite H; auto. f_equal.
+    rewrite !map_map_compose. apply_spec. intros.
+    unfold compose. auto.
+  - rewrite add_assoc, H0; auto. f_equal. now f_equal.
+  - rewrite add_assoc, H0; auto. f_equal. now f_equal.
+Qed.
+
+Lemma distr_subst :
+  forall (P : term) (wfP : wf P) N M k,
+    subst_rec P (subst0 N M) k = subst0 (subst_rec P N k) (subst_rec P M (S k)).
+Proof.
+  intros; unfold subst in |- *.
+  pattern k at 1 3 in |- *.
+  change k with (0 + k).
+  now apply distr_subst_rec.
+Qed.
+
+
+Lemma lift_closed n k t : closedn k t = true -> lift n k t = t.
+Proof.
+  revert k.
+  elim t using term_forall_list_ind; intros; try easy;
+    rewrite ?map_map_compose, ?compose_on_snd, ?compose_map_def;
+    try (f_equal; apply_spec);  simpl closed in *;
+    try rewrite ?map_length; try easy.
+  - rewrite lift_rel_lt; auto.
+    revert H. elim (Nat.ltb_spec n0 k); intros; try easy.
+  - simpl lift; f_equal.
+    rewrite <- map_id. 
+    apply_spec; eauto.
+  - simpl lift. rewrite andb_true_iff in H1. f_equal; intuition eauto.
+  - simpl lift; rewrite andb_true_iff in H1. f_equal; intuition eauto.
+  - simpl lift. rewrite !andb_true_iff in H2. f_equal; intuition eauto.
+  - simpl lift. rewrite !andb_true_iff in H1. f_equal; intuition eauto.
+    rewrite <- map_id; apply_spec; eauto.
+  - simpl lift. rewrite !andb_true_iff in H2. f_equal; intuition eauto.
+    transitivity (map (on_snd id) l). apply_spec; eauto.
+    rewrite <- map_id. f_equal. unfold on_snd. extensionality p. now destruct p.
+  - simpl lift. f_equal; eauto.
+  - simpl lift. f_equal.
+    transitivity (map (map_def id) m). apply_spec; eauto.
+    now autorewrite with core.
+  - simpl lift. f_equal.
+    transitivity (map (map_def id) m). apply_spec; eauto.
+    now autorewrite with core.
+Qed.
diff --git a/extraction/theories/Typing.v b/extraction/theories/Typing.v
new file mode 100644
index 000000000..ca85646d8
--- /dev/null
+++ b/extraction/theories/Typing.v
@@ -0,0 +1,164 @@
+(* Distributed under the terms of the MIT license.   *)
+
+From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
+Require Import Template.config Template.utils Template.kernel.univ.
+From TemplateExtraction Require Import Ast Induction LiftSubst UnivSubst.
+Require Import String.
+Local Open Scope string_scope.
+Set Asymmetric Patterns.
+
+
+(** * Typing derivations
+
+  *WIP*
+
+  Inductive relations for reduction, conversion and typing of CIC terms.
+
+ *)
+
+(** ** Environment lookup *)
+
+Definition global_decl_ident d :=
+  match d with
+  | ConstantDecl id _ => id
+  | InductiveDecl id _ => id
+  end.
+
+Definition is_constant_decl d :=
+  match d with
+  | InductiveDecl _ _ => false
+  | _ => true
+  end.
+
+Definition is_minductive_decl d :=
+  match d with
+  | InductiveDecl _ _ => true
+  | _ => false
+  end.
+
+Definition is_inductive_decl_for i d :=
+  match d with
+  | InductiveDecl _ cb => i < List.length cb.(ind_bodies)
+  | _ => False
+  end.
+
+Definition ident_eq (x y : ident) :=
+  if string_dec x y then true else false.
+
+Lemma ident_eq_spec x y : reflect (x = y) (ident_eq x y).
+Proof.
+  unfold ident_eq. destruct string_dec; constructor; auto.
+Qed.
+
+Fixpoint lookup_env (Σ : global_declarations) (id : ident) : option global_decl :=
+  match Σ with
+  | nil => None
+  | hd :: tl =>
+    if ident_eq id (global_decl_ident hd) then Some hd
+    else lookup_env tl id
+  end.
+
+Definition declared_constant (Σ : global_declarations) (id : ident) decl : Prop :=
+  lookup_env Σ id = Some (ConstantDecl id decl).
+
+Definition declared_minductive Σ mind decl :=
+  lookup_env Σ mind = Some (InductiveDecl mind decl).
+
+Definition declared_inductive Σ ind univs decl :=
+  exists decl', declared_minductive Σ (inductive_mind ind) decl' /\
+                univs = decl'.(ind_universes) /\
+                List.nth_error decl'.(ind_bodies) (inductive_ind ind) = Some decl.
+
+Definition declared_constructor Σ cstr univs decl : Prop :=
+  let '(ind, k) := cstr in
+  exists decl', declared_inductive Σ ind univs decl' /\
+                List.nth_error decl'.(ind_ctors) k = Some decl.
+
+Definition declared_projection Σ (proj : projection) decl : Prop :=
+  let '(ind, ppars, arg) := proj in
+  exists univs decl', declared_inductive Σ ind univs decl' /\
+                List.nth_error decl'.(ind_projs) arg = Some decl.
+
+Program
+Definition type_of_constant_decl (d : global_decl | is_constant_decl d = true) : term :=
+  match d with
+  | InductiveDecl _ _ => !
+  | ConstantDecl _ decl => decl.(cst_type)
+  end.
+
+Program
+Definition body_of_constant_decl (d : global_decl | is_constant_decl d = true) : option term :=
+  match d with
+  | InductiveDecl _ _ => !
+  | ConstantDecl _ decl => decl.(cst_body)
+  end.
+
+Program
+Definition types_of_minductive_decl (d : global_decl | is_minductive_decl d = true) :
+  list one_inductive_body :=
+  match d with
+  | InductiveDecl _ tys => tys.(ind_bodies)
+  | ConstantDecl _ _ => !
+  end.
+
+Definition inds ind u (l : list one_inductive_body) :=
+  let fix aux n :=
+      match n with
+      | 0 => []
+      | S n => tInd (mkInd ind n) u :: aux n
+      end
+  in aux (List.length l).
+
+Program
+Definition type_of_constructor (Σ : global_declarations) (c : inductive * nat) (univs : universe_context) (u : list Level.t) (decl : ident * term * nat)
+           (H : declared_constructor Σ c univs decl) :=
+  let mind := inductive_mind (fst c) in
+  let '(id, trm, args) := decl in
+  match lookup_env Σ mind with
+  | Some (InductiveDecl _ decl') =>
+    substl (inds mind u decl'.(ind_bodies)) (subst_instance_constr u trm)
+  | _ => !
+  end.
+
+Next Obligation.
+  destruct H as [decl [H H']].
+  destruct H as [decl' [H'' H''']].
+  eapply H0.
+  simpl. rewrite H''. reflexivity.
+Defined.
+
+(** ** Reduction *)
+
+(** *** Helper functions for reduction *)
+
+Definition fix_subst (l : mfixpoint term) :=
+  let fix aux n :=
+      match n with
+      | 0 => []
+      | S n => tFix l n :: aux n
+      end
+  in aux (List.length l).
+
+Definition unfold_fix (mfix : mfixpoint term) (idx : nat) :=
+  match List.nth_error mfix idx with
+  | Some d => Some (d.(rarg), substl (fix_subst mfix) d.(dbody))
+  | None => None
+  end.
+
+Definition is_constructor n ts :=
+  match List.nth_error ts n with
+  | Some a =>
+    match a with
+    | tConstruct _ _ _ => true
+    | tApp (tConstruct _ _ _) _ => true
+    | _ => false
+    end
+  | None => false
+  end.
+
+Definition tDummy := tRel 0.
+
+Definition iota_red npar c args brs :=
+  (mkApps (snd (List.nth c brs (0, tDummy))) (List.skipn npar args)).
+
+Notation "#| Γ |" := (List.length Γ) (at level 0, Γ at level 99, format "#| Γ |").
diff --git a/extraction/theories/UnivSubst.v b/extraction/theories/UnivSubst.v
new file mode 100644
index 000000000..d98b6ca03
--- /dev/null
+++ b/extraction/theories/UnivSubst.v
@@ -0,0 +1,72 @@
+(* Distributed under the terms of the MIT license.   *)
+
+From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
+From Template Require Import utils univ.
+From TemplateExtraction Require Import Ast Induction LiftSubst.
+From Template Require AstUtils.
+Require Import String.
+Local Open Scope string_scope.
+Set Asymmetric Patterns.
+
+(** * Universe substitution
+
+  *WIP*
+
+  Substitution of universe levels for universe level variables, used to
+  implement universe polymorphism. *)
+
+Definition subst_instance_level u l :=
+  match l with
+  | univ.Level.lProp | univ.Level.lSet | univ.Level.Level _ => l
+  | univ.Level.Var n => List.nth n u univ.Level.lProp
+  end.
+
+Definition subst_instance_cstrs u cstrs :=
+  ConstraintSet.fold (fun '(l,d,r) =>
+                     ConstraintSet.add (subst_instance_level u l, d, subst_instance_level u r))
+                  cstrs ConstraintSet.empty.
+
+Definition subst_instance_level_expr (u : universe_instance) (s : Universe.Expr.t) :=
+  let '(l, b) := s in (subst_instance_level u l, b).
+
+Definition subst_instance_univ (u : universe_instance) (s : universe) :=
+  List.map (subst_instance_level_expr u) s.
+
+Definition subst_instance_instance (u u' : universe_instance) :=
+  List.map (subst_instance_level u) u'.
+
+Fixpoint subst_instance_constr (u : universe_instance) (c : term) :=
+  match c with
+  | tBox | tRel _ | tVar _ | tMeta _ => c
+  | tSort s => tSort (subst_instance_univ u s)
+  | tConst c u' => tConst c (subst_instance_instance u u')
+  | tInd i u' => tInd i (subst_instance_instance u u')
+  | tConstruct ind k u' => tConstruct ind k (subst_instance_instance u u')
+  | tEvar ev args => tEvar ev (List.map (subst_instance_constr u) args)
+  | tLambda na T M => tLambda na (subst_instance_constr u T) (subst_instance_constr u M)
+  | tApp f v => tApp (subst_instance_constr u f) (List.map (subst_instance_constr u) v)
+  | tProd na A B => tProd na (subst_instance_constr u A) (subst_instance_constr u B)
+  | tLetIn na b ty b' => tLetIn na (subst_instance_constr u b) (subst_instance_constr u ty)
+                                (subst_instance_constr u b')
+  | tCase ind p c brs =>
+    let brs' := List.map (on_snd (subst_instance_constr u)) brs in
+    tCase ind (subst_instance_constr u p) (subst_instance_constr u c) brs'
+  | tProj p c => tProj p (subst_instance_constr u c)
+  | tFix mfix idx =>
+    let mfix' := List.map (map_def (subst_instance_constr u)) mfix in
+    tFix mfix' idx
+  | tCoFix mfix idx =>
+    let mfix' := List.map (map_def (subst_instance_constr u)) mfix in
+    tCoFix mfix' idx
+  end.
+
+Definition map_decl f (d : context_decl) :=
+  {| decl_name := d.(decl_name);
+     decl_body := option_map f d.(decl_body);
+     decl_type := f d.(decl_type) |}.
+
+Definition map_context f c :=
+  List.map (map_decl f) c.
+
+Definition subst_instance_context (u : universe_instance) (c : context) : context :=
+  map_context (subst_instance_constr u) c.
\ No newline at end of file
diff --git a/extraction/theories/WcbvEval.v b/extraction/theories/WcbvEval.v
new file mode 100644
index 000000000..06547fe94
--- /dev/null
+++ b/extraction/theories/WcbvEval.v
@@ -0,0 +1,305 @@
+(* Distributed under the terms of the MIT license.   *)
+
+From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
+From Template Require Import config utils Ast univ.
+From TemplateExtraction Require Import Ast Induction LiftSubst UnivSubst Typing.
+From Template Require AstUtils.
+Require Import String.
+Local Open Scope string_scope.
+Set Asymmetric Patterns.
+
+Existing Instance config.default_checker_flags.
+
+
+(** * Weak (head) call-by-value evaluation strategy.
+
+  The [wcbveval] inductive relation specifies weak cbv evaluation.  It
+  is shown to be a subrelation of the 1-step reduction relation from
+  which conversion is defined. Hence two terms that reduce to the same
+  wcbv head normal form are convertible.
+
+  This reduction strategy is supposed to mimick at the Coq level the
+  reduction strategy of ML programming languages. It is used to state
+  the extraction conjecture that can be applied to Coq terms to produce
+  (untyped) terms where all proofs are erased to a dummy value. *)
+
+(** Helpers for reduction *)
+
+Definition iota_red npar c args brs :=
+  (mkApps (snd (List.nth c brs (0, tBox))) (List.skipn npar args)).
+
+Definition fix_subst (l : mfixpoint term) :=
+  let fix aux n :=
+      match n with
+      | 0 => []
+      | S n => tFix l n :: aux n
+      end
+  in aux (List.length l).
+
+Definition unfold_fix (mfix : mfixpoint term) (idx : nat) :=
+  match List.nth_error mfix idx with
+  | Some d => Some (d.(rarg), substl (fix_subst mfix) d.(dbody))
+  | None => None
+  end.
+
+Definition is_constructor n ts :=
+  match List.nth_error ts n with
+  | Some a =>
+    match a with
+    | tConstruct _ _ _ => true
+    | tApp (tConstruct _ _ _) _ => true
+    | _ => false
+    end
+  | None => false
+  end.
+
+
+Definition mktApp f l :=
+  match l with
+  | nil => f
+  | l => tApp f l
+  end.
+
+(** ** Big step version of weak cbv beta-zeta-iota-fix-delta reduction.
+
+  TODO: CoFixpoints *)
+
+Section Wcbv.
+  Context (Σ : global_declarations) (Γ : context).
+  (* The local context is fixed: we are only doing weak reductions *)
+
+  Inductive eval : term -> term -> Prop :=
+  (** Reductions *)
+  | eval_box l : eval (mktApp tBox l) tBox
+
+  (** Beta *)
+  | eval_beta f na t b a a' l res :
+      eval f (tLambda na t b) ->
+      eval a a' ->
+      eval (mkApps (subst0 a' b) l) res ->
+      eval (tApp f (a :: l)) res
+
+  (** Let *)
+  | eval_zeta na b0 b0' t b1 res :
+      eval b0 b0' ->
+      eval (subst0 b0' b1) res ->
+      eval (tLetIn na b0 t b1) res
+
+  (** Local variables: defined or undefined *)
+  | eval_rel_def i (isdecl : i < List.length Γ) body res :
+      (safe_nth Γ (exist _ i isdecl)).(decl_body) = Some body ->
+      eval (lift0 (S i) body) res ->
+      eval (tRel i) res
+
+  | eval_rel_undef i (isdecl : i < List.length Γ) :
+      (safe_nth Γ (exist _ i isdecl)).(decl_body) = None ->
+      eval (tRel i) (tRel i)
+
+  (** Case *)
+  | eval_iota ind pars discr c u args p brs res :
+      eval discr (mkApps (tConstruct ind c u) args) ->
+      eval (iota_red pars c args brs) res ->
+      eval (tCase (ind, pars) p discr brs) res
+
+  (** Fix unfolding, with guard *)
+  | eval_fix mfix idx args args' narg fn res :
+      unfold_fix mfix idx = Some (narg, fn) ->
+      Forall2 eval args args' -> (* FIXME should we reduce the args after the recursive arg here? *)
+      is_constructor narg args' = true ->
+      eval (mkApps fn args') res ->
+      eval (mkApps (tFix mfix idx) args) res
+
+  (** Constant unfolding *)
+  | eval_delta c decl body (isdecl : declared_constant Σ c decl) u res :
+      decl.(cst_body) = Some body ->
+      eval (subst_instance_constr u body) res ->
+      eval (tConst c u) res
+
+  (** Proj *)
+  | eval_proj i pars arg discr args k u res :
+      eval discr (mkApps (tConstruct i k u) args) ->
+      eval (List.nth (pars + arg) args tDummy) res ->
+      eval (tProj (i, pars, arg) discr) res
+
+  (* TODO CoFix *)
+  | eval_abs na M N : eval (tLambda na M N) (tLambda na M N)
+
+  | eval_prod na b t b' t' :
+      eval b b' -> eval t t' -> eval (tProd na b t) (tProd na b' t')
+
+  | eval_ind_ i u : eval (tInd i u) (tInd i u)
+
+  | eval_app_ind t i u l l' : l <> nil ->
+      eval t (tInd i u) ->
+      Forall2 eval l l' ->
+      eval (tApp t l) (tApp (tInd i u) l')
+
+  | eval_constr i k u :
+      eval (tConstruct i k u) (tConstruct i k u)
+
+  | eval_app_constr f i k u l l' : l <> nil ->
+      eval f (tConstruct i k u) ->
+      Forall2 eval l l' ->
+      eval (tApp f l) (tApp (tConstruct i k u) l')
+
+  (* | evar ev l l' : evals l l' -> eval (tEvar ev l) (tEvar ev l') *)
+  | eval_evar ev l : eval (tEvar ev l) (tEvar ev l) (* Lets say it is a value for now *).
+
+  (** The right induction principle for the nested [Forall] cases: *)
+
+  Lemma eval_evals_ind :
+    forall P : term -> term -> Prop,
+      (forall l, P (mktApp tBox l) tBox) ->
+      (forall (f : term) (na : name) (t b a a' : term) (l : list term) (res : term),
+          eval f (tLambda na t b) ->
+          P f (tLambda na t b) ->
+          eval a a' -> P a a' ->
+          eval (mkApps (b {0 := a'}) l) res -> P (mkApps (b {0 := a'}) l) res -> P (tApp f (a :: l)) res) ->
+
+      (forall (na : name) (b0 b0' t b1 res : term),
+          eval b0 b0' -> P b0 b0' -> eval (b1 {0 := b0'}) res -> P (b1 {0 := b0'}) res -> P (tLetIn na b0 t b1) res) ->
+
+      (forall (i : nat) (isdecl : i < #|Γ|) (body res : term),
+          decl_body (safe_nth Γ (exist (fun n : nat => n < #|Γ|) i isdecl)) = Some body ->
+          eval ((lift0 (S i)) body) res -> P ((lift0 (S i)) body) res -> P (tRel i) res) ->
+
+      (forall (i : nat) (isdecl : i < #|Γ|),
+          decl_body (safe_nth Γ (exist (fun n : nat => n < #|Γ|) i isdecl)) = None -> P (tRel i) (tRel i)) ->
+
+      (forall (ind : inductive) (pars : nat) (discr : term) (c : nat) (u : universe_instance)
+              (args : list term) (p : term) (brs : list (nat * term)) (res : term),
+          eval discr (mkApps (tConstruct ind c u) args) ->
+          P discr (mkApps (tConstruct ind c u) args) ->
+          eval (iota_red pars c args brs) res ->
+          P (iota_red pars c args brs) res -> P (tCase (ind, pars) p discr brs) res) ->
+
+      (forall (mfix : mfixpoint term) (idx : nat) (args args' : list term) (narg : nat) (fn res : term),
+          unfold_fix mfix idx = Some (narg, fn) ->
+          Forall2 eval args args' ->
+          Forall2 P args args' ->
+          is_constructor narg args' = true ->
+          eval (mkApps fn args') res -> P (mkApps fn args') res -> P (mkApps (tFix mfix idx) args) res) ->
+
+      (forall (c : ident) (decl : constant_body) (body : term),
+          declared_constant Σ c decl ->
+          forall (u : universe_instance) (res : term),
+            cst_body decl = Some body ->
+            eval (subst_instance_constr u body) res -> P (subst_instance_constr u body) res -> P (tConst c u) res) ->
+
+      (forall (i : inductive) (pars arg : nat) (discr : term) (args : list term) (k : nat)
+              (u : universe_instance) (res : term),
+          eval discr (mkApps (tConstruct i k u) args) ->
+          P discr (mkApps (tConstruct i k u) args) ->
+          eval (nth (pars + arg) args tDummy) res ->
+          P (nth (pars + arg) args tDummy) res -> P (tProj (i, pars, arg) discr) res) ->
+
+      (forall (na : name) (M N : term), P (tLambda na M N) (tLambda na M N)) ->
+
+      (forall (na : name) (M M' N N' : term),
+          eval M M' -> eval N N' -> P M M' -> P N N' ->
+          P (tProd na M N) (tProd na M' N')) ->
+
+      (forall i u, P (tInd i u) (tInd i u)) ->
+
+      (forall (f8 : term) (i : inductive) (u : universe_instance) (l l' : list term),
+          l <> nil -> eval f8 (tInd i u) ->
+          P f8 (tInd i u) -> Forall2 eval l l' -> Forall2 P l l' -> P (tApp f8 l) (tApp (tInd i u) l')) ->
+
+      (forall i k u, P (tConstruct i k u) (tConstruct i k u)) ->
+
+      (forall (f8 : term) (i : inductive) (k : nat) (u : universe_instance) (l l' : list term),
+          l <> nil -> eval f8 (tConstruct i k u) ->
+          P f8 (tConstruct i k u) -> Forall2 eval l l' -> Forall2 P l l' -> P (tApp f8 l) (tApp (tConstruct i k u) l')) ->
+
+      (forall (ev : nat) (l : list term), P (tEvar ev l) (tEvar ev l)) ->
+
+      forall t t0 : term, eval t t0 -> P t t0.
+  Proof.
+    intros P Hbox Hbeta Hlet Hreldef Hrelvar Hcase Hfix Hconst Hproj Hlam Hprod Hind Hindapp Hcstr Hcstrapp Hevar.
+    fix 3. destruct 1;
+             try match goal with [ H : _ |- _ ] =>
+                             match type of H with
+                               forall t t0, eval t t0 -> _ => fail 1
+                             | _ => eapply H
+                             end end; eauto.
+    clear H1 H2.
+    revert args args' H0. fix aux 3. destruct 1. constructor; auto.
+    constructor. now apply eval_evals_ind. now apply aux.
+    revert l l' H H1. fix aux 4. destruct 2. contradiction. constructor.
+    now apply eval_evals_ind.
+    destruct l. inv H2; constructor.
+    now apply aux.
+    revert l l' H H1. fix aux 4. destruct 2. contradiction. constructor.
+    now apply eval_evals_ind. destruct l. inv H2; constructor. now apply aux.
+  Defined.
+
+  (** Characterization of values for this reduction relation:
+      Basically atoms (constructors, inductives, products (FIXME sorts missing))
+      and de Bruijn variables and lambda abstractions. Closed values disallow
+      de Bruijn variables. *)
+
+  Inductive value : term -> Prop :=
+  | value_tBox : value tBox
+  | value_tRel i : value (tRel i)
+  | value_tEvar ev l : value (tEvar ev l)
+  | value_tLam na t b : value (tLambda na t b)
+  | value_tProd na t u : value (tProd na t u)
+  | value_tInd i k l : List.Forall value l -> value (mkApps (tInd i k) l)
+  | value_tConstruct i k u l : List.Forall value l -> value (mkApps (tConstruct i k u) l).
+
+  Lemma value_values_ind : forall P : term -> Prop,
+      (P tBox) ->
+       (forall i : nat, P (tRel i)) ->
+       (forall (ev : nat) (l : list term), P (tEvar ev l)) ->
+       (forall (na : name) (t b : term), P (tLambda na t b)) ->
+       (forall (na : name) (t u : term), P (tProd na t u)) ->
+       (forall (i : inductive) (k : universe_instance) l, List.Forall value l -> List.Forall P l -> P (mkApps (tInd i k) l)) ->
+       (forall (i : inductive) (k : nat) (u : universe_instance) (l : list term),
+        List.Forall value l -> List.Forall P l -> P (mkApps (tConstruct i k u) l)) -> forall t : term, value t -> P t.
+  Proof.
+    intros P ???????.
+    fix value_values_ind 2. destruct 1. 1-4:clear value_values_ind; auto.
+    apply H3. apply H4. apply H6.
+    revert l H6. fix aux 2. destruct 1. constructor; auto.
+    constructor. now apply value_values_ind. now apply aux.
+    apply H5. apply H6.
+    revert l H6. fix aux 2. destruct 1. constructor; auto.
+    constructor. now apply value_values_ind. now apply aux.
+  Defined.
+
+  (** The codomain of evaluation is only values:
+      It means no redex can remain at the head of an evaluated term. *)
+
+  Lemma Forall2_right {A B} (P : B -> Prop) (l : list A) (l' : list B) :
+    Forall2 (fun x y => P y) l l' -> List.Forall (fun x => P x) l'.
+  Proof.
+    induction 1; constructor; auto.
+  Qed.
+
+  Lemma Forall2_non_nil {A B} (P : A -> B -> Prop) (l : list A) (l' : list B) :
+    Forall2 P l l' -> l <> nil -> l' <> nil.
+  Proof.
+    induction 1; congruence.
+  Qed.
+
+  Lemma eval_to_value e e' : eval e e' -> value e'.
+  Proof.
+    induction 1 using eval_evals_ind; simpl; auto using value.
+    eapply (value_tInd i u []); try constructor.
+    pose proof (value_tInd i u l'). forward H3.
+    apply (Forall2_right _ _ _ H2).
+    rewrite mkApps_tApp in H3; auto. simpl; auto. eauto using Forall2_non_nil.
+    eapply (value_tConstruct i k u []); try constructor.
+    pose proof (value_tConstruct i k u l'). forward H3.
+    apply (Forall2_right _ _ _ H2).
+    rewrite mkApps_tApp in H3; auto. simpl; auto. eauto using Forall2_non_nil.
+  Qed.
+
+  (** Evaluation preserves closedness: *)
+  Lemma eval_closed : forall n t u, closedn n t = true -> eval t u -> closedn n u = true.
+  Proof.
+    induction 2 using eval_evals_ind; simpl in *; eauto. eapply IHeval3.
+    admit.
+  Admitted. (* FIXME complete *)
+
+End Wcbv.
diff --git a/template-coq/_CoqProject b/template-coq/_CoqProject
index 2470ba5e3..9692092b4 100644
--- a/template-coq/_CoqProject
+++ b/template-coq/_CoqProject
@@ -23,7 +23,10 @@ theories/LiftSubst.v
 theories/WeakSubst.v
 theories/UnivSubst.v
 theories/Typing.v
+theories/MetaTheory.v
 theories/Checker.v
+theories/WcbvEval.v
+theories/Retyping.v
 theories/All.v
 theories/Extraction.v
 
diff --git a/template-coq/theories/Ast.v b/template-coq/theories/Ast.v
index e00d442f6..70d58f71e 100644
--- a/template-coq/theories/Ast.v
+++ b/template-coq/theories/Ast.v
@@ -102,6 +102,32 @@ Definition mkApps t us :=
 
 Definition mkApp t u := Eval cbn in mkApps t [u].
 
+Definition isApp t :=
+  match t with
+  | tApp _ _ => true
+  | _ => false
+  end.
+
+(** Well-formed terms: invariants which are not ensured by the OCaml type system *)
+
+Inductive wf : term -> Prop :=
+| wf_tRel n : wf (tRel n)
+| wf_tVar id : wf (tVar id)
+| wf_tMeta n : wf (tMeta n)
+| wf_tEvar n l : Forall wf l -> wf (tEvar n l)
+| wf_tSort u : wf (tSort u)
+| wf_tCast t k t' : wf t -> wf t' -> wf (tCast t k t')
+| wf_tProd na t b : wf t -> wf b -> wf (tProd na t b)
+| wf_tLambda na t b : wf t -> wf b -> wf (tLambda na t b)
+| wf_tLetIn na t b b' : wf t -> wf b -> wf b' -> wf (tLetIn na t b b')
+| wf_tApp t u : ~ isApp t = true -> u <> nil -> wf t -> Forall wf u -> wf (tApp t u)
+| wf_tConst k u : wf (tConst k u)
+| wf_tInd i u : wf (tInd i u)
+| wf_tConstruct i k u : wf (tConstruct i k u)
+| wf_tCase ci p c brs : wf p -> wf c -> Forall (Program.Basics.compose wf snd) brs -> wf (tCase ci p c brs)
+| wf_tProj p t : wf t -> wf (tProj p t)
+| wf_tFix mfix k : Forall (fun def => wf def.(dtype _) /\ wf def.(dbody _)) mfix -> wf (tFix mfix k)
+| wf_tCoFix mfix k : Forall (fun def => wf def.(dtype _) /\ wf def.(dbody _)) mfix -> wf (tCoFix mfix k).
 
 (** ** Entries
 
diff --git a/template-coq/theories/Checker.v b/template-coq/theories/Checker.v
index 2de912140..cb48244a2 100644
--- a/template-coq/theories/Checker.v
+++ b/template-coq/theories/Checker.v
@@ -509,8 +509,6 @@ Instance monad_exc : MonadExc type_error typing_result :=
       end
   }.
 
-Class Fuel := { fuel : nat }.
-
 Definition check_conv_gen `{checker_flags} {F:Fuel} conv_pb Σ Γ t u :=
   match isconv Σ fuel conv_pb Γ t [] u [] with
   | Some b => if b then ret () else raise (NotConvertible Γ t u t u)
diff --git a/template-coq/theories/ErasedTerm.v b/template-coq/theories/ErasedTerm.v
new file mode 100644
index 000000000..fffe258b5
--- /dev/null
+++ b/template-coq/theories/ErasedTerm.v
@@ -0,0 +1,34 @@
+(* Distributed under the terms of the MIT license.   *)
+
+Require Import Coq.Strings.String.
+Require Import Coq.PArith.BinPos.
+Require Import List. Import ListNotations.
+From Template Require Import monad_utils.
+From Template Require Export univ uGraph Ast.
+
+(** Erased terms
+
+  These are the terms produced by erasure:
+  compared to kernel terms, all proofs are translated to [tBox] and
+  casts are removed.
+*)
+
+Inductive term : Set :=
+| tBox       : term (* Represents all proofs *)
+| tRel       : nat -> term
+| tVar       : ident -> term (* For free variables (e.g. in a goal) *)
+| tMeta      : nat -> term   (* NOTE: this will go away *)
+| tEvar      : nat -> list term -> term
+| tSort      : universe -> term
+| tProd      : name -> term (* the type *) -> term -> term
+| tLambda    : name -> term -> term -> term
+| tLetIn     : name -> term (* the term *) -> term -> term -> term
+| tApp       : term -> list term -> term
+| tConst     : kername -> universe_instance -> term
+| tInd       : inductive -> universe_instance -> term
+| tConstruct : inductive -> nat -> universe_instance -> term
+| tCase      : (inductive * nat) (* # of parameters *) -> term (* type info *)
+               -> term (* discriminee *) -> list (nat * term) (* branches *) -> term
+| tProj      : projection -> term -> term
+| tFix       : mfixpoint term -> nat -> term
+| tCoFix     : mfixpoint term -> nat -> term.
diff --git a/template-coq/theories/Induction.v b/template-coq/theories/Induction.v
index 3c4384cfd..2d1ee9c27 100644
--- a/template-coq/theories/Induction.v
+++ b/template-coq/theories/Induction.v
@@ -253,3 +253,83 @@ Ltac apply_spec :=
   | H : tFixProp _ _ |- map _ _ = map _ _ =>
     eapply (tfix_map_spec H)
   end.
+
+Lemma lift_to_list (P : term -> Prop) : (forall t, wf t -> P t) -> forall l, Forall wf l -> Forall P l.
+Proof.
+  intros IH.
+  fix 1.
+  destruct l; constructor.
+  apply IH. now inversion_clear H.
+  apply lift_to_list. now inversion_clear H.
+Defined.
+
+Lemma lift_to_wf_list (P : term -> Prop) : forall l, Forall (fun t => wf t -> P t) l -> Forall wf l -> Forall P l.
+Proof.
+  induction 1. constructor.
+  inversion_clear 1. specialize (IHForall H3).
+  constructor; auto.
+Qed.
+
+Ltac inv H := inversion_clear H.
+Lemma term_wf_forall_list_ind :
+  forall P : term -> Prop,
+    (forall n : nat, P (tRel n)) ->
+    (forall i : ident, P (tVar i)) ->
+    (forall n : nat, P (tMeta n)) ->
+    (forall (n : nat) (l : list term), Forall P l -> P (tEvar n l)) ->
+    (forall s, P (tSort s)) ->
+    (forall t : term, P t -> forall (c : cast_kind) (t0 : term), P t0 -> P (tCast t c t0)) ->
+    (forall (n : name) (t : term), P t -> forall t0 : term, P t0 -> P (tProd n t t0)) ->
+    (forall (n : name) (t : term), P t -> forall t0 : term, P t0 -> P (tLambda n t t0)) ->
+    (forall (n : name) (t : term),
+        P t -> forall t0 : term, P t0 -> forall t1 : term, P t1 -> P (tLetIn n t t0 t1)) ->
+    (forall t : term, ~ isApp t = true -> P t -> forall l : list term, l <> nil -> Forall P l -> P (tApp t l)) ->
+    (forall (s : String.string) (u : list Level.t), P (tConst s u)) ->
+    (forall (i : inductive) (u : list Level.t), P (tInd i u)) ->
+    (forall (i : inductive) (n : nat) (u : list Level.t), P (tConstruct i n u)) ->
+    (forall (p : inductive * nat) (t : term),
+        P t -> forall t0 : term, P t0 -> forall l : list (nat * term),
+            tCaseBrsProp P l -> P (tCase p t t0 l)) ->
+    (forall (s : projection) (t : term), P t -> P (tProj s t)) ->
+    (forall (m : mfixpoint term) (n : nat), tFixProp P m -> P (tFix m n)) ->
+    (forall (m : mfixpoint term) (n : nat), tFixProp P m -> P (tCoFix m n)) ->
+    forall t : term, wf t -> P t.
+Proof.
+  intros until t. revert t.
+  apply (term_forall_list_ind (fun t => wf t -> P t));
+    intros; try solve [match goal with
+                 H : _ |- _ => apply H
+              end; auto].
+  apply H2. inv H17.
+  auto using lift_to_wf_list.
+
+  inv H18; auto.
+  inv H18; auto.
+  inv H18; auto.
+  inv H19; auto.
+  inv H18; auto.
+
+  apply H8; auto.
+  auto using lift_to_wf_list.
+
+  inv H19; apply H12; auto.
+  red.
+  red in H18.
+  induction H18.
+  constructor.
+  inv H22; auto.
+
+  inv H17; auto.
+
+  inv H17; auto.
+  apply H14. red.
+  red in H16.
+  induction H16. constructor.
+  inv H18; constructor; intuition auto.
+
+  inv H17; auto.
+  apply H15. red.
+  red in H16.
+  induction H16. constructor.
+  inv H18; constructor; intuition auto.
+Qed.
diff --git a/template-coq/theories/LiftSubst.v b/template-coq/theories/LiftSubst.v
index b82b54777..67b8b068b 100644
--- a/template-coq/theories/LiftSubst.v
+++ b/template-coq/theories/LiftSubst.v
@@ -52,7 +52,7 @@ Fixpoint subst t k u :=
     end
   | tEvar ev args => tEvar ev (List.map (subst t k) args)
   | tLambda na T M => tLambda na (subst t k T) (subst t (S k) M)
-  | tApp u v => tApp (subst t k u) (List.map (subst t k) v)
+  | tApp u v => mkApps (subst t k u) (List.map (subst t k) v)
   | tProd na A B => tProd na (subst t k A) (subst t (S k) B)
   | tCast c kind ty => tCast (subst t k c) kind (subst t k ty)
   | tLetIn na b ty b' => tLetIn na (subst t k b) (subst t k ty) (subst t (S k) b')
@@ -147,6 +147,11 @@ Proof.
   now elim (leb_spec p n).
 Qed.
 
+Lemma lift_rel_alt : forall n k i, lift n k (tRel i) = tRel (if Nat.leb k i then n + i else i).
+Proof.
+  intros; simpl. now destruct leb.
+Qed.
+
 Lemma subst_rel_lt : forall u n k, k > n -> subst_rec u (tRel n) k = tRel n.
 Proof.
   simpl in |- *; intros.
@@ -243,13 +248,67 @@ Lemma permute_lift :
   apply permute_lift_rec; easy.
 Qed.
 
+Lemma Forall_map {A B} (P : B -> Prop) (f : A -> B) l : Forall (Program.Basics.compose P f) l -> Forall P (map f l).
+Proof.
+  induction 1; constructor; auto.
+Qed.
+
+Lemma Forall_impl {A} (P Q : A -> Prop) : forall l, Forall P l -> (forall x, P x -> Q x) -> Forall Q l.
+Proof.
+  induction 1; constructor; auto.
+Qed.
+
+Lemma lift_rec_isApp n k t : ~ isApp t = true -> ~ isApp (lift n k t) = true.
+Proof.
+  induction t; auto.
+  intros.
+  simpl. destruct leb; auto.
+Qed.
+
+Lemma map_non_nil {A B} (f : A -> B) l : l <> nil -> map f l <> nil.
+Proof.
+  intros. intro.
+  destruct l; try discriminate.
+  contradiction.
+Qed.
+
+Lemma lift_rec_wf n k t : wf t -> wf (lift_rec n t k).
+Proof.
+  intros wft; revert t wft k.
+  apply (term_wf_forall_list_ind (fun t => forall k, wf (lift n k t))) ; simpl; intros; try constructor; auto.
+
+  destruct leb; constructor.
+  apply Forall_map.
+  induction H; constructor; auto.
+  now apply lift_rec_isApp.
+  now apply map_non_nil.
+  apply Forall_map. eapply Forall_impl. apply H2. auto.
+  apply Forall_map. eapply Forall_impl. apply H1.
+  intros [n' t]. simpl. repeat red; simpl; auto.
+  apply Forall_map. eapply Forall_impl. apply H.
+  simpl. intros. red; intuition (simpl; auto).
+  apply Forall_map. eapply Forall_impl. apply H.
+  simpl. intros. red; intuition (simpl; auto).
+Qed.
+
+Lemma mkApps_tApp t l :
+  ~ isApp t = true -> l <> nil -> mkApps t l = tApp t l.
+Proof.
+  intros.
+  destruct l. simpl. contradiction.
+  destruct t; simpl; try reflexivity.
+  simpl in H. contradiction.
+Qed.
+
+Hint Unfold compose.
+Hint Transparent compose.
+
 Lemma simpl_subst_rec :
-  forall M N n p k,
+  forall M (H : wf M) N n p k,
     p <= n + k ->
     k <= p -> subst_rec N (lift_rec (S n) M k) p = lift_rec n M k.
 Proof.
-  intros M.
-  elim M using term_forall_list_ind;
+  intros M wfM. induction wfM using term_wf_forall_list_ind;
     intros; simpl; try easy;
       rewrite ?map_map_compose, ?compose_on_snd, ?compose_map_def;
       try solve [f_equal; easy];
@@ -260,13 +319,36 @@ Proof.
   - elim (leb_spec k n); intros; try easy.
     + rewrite subst_rel_gt; try easy.
     + rewrite subst_rel_lt; try easy.
+
+  - rewrite IHwfM; auto.
+    apply (lift_rec_isApp n k) in H.
+    rewrite mkApps_tApp; auto using map_non_nil.
+    f_equal. eapply forall_map_spec. apply H1; simpl; auto.
+    simpl; intros. typeclasses eauto with core.
 Qed.
 
 Lemma simpl_subst :
-  forall N M n p, p <= n -> subst_rec N (lift0 (S n) M) p = lift0 n M.
+  forall N M (H : wf M) n p, p <= n -> subst_rec N (lift0 (S n) M) p = lift0 n M.
   intros; now apply simpl_subst_rec.
 Qed.
 
+Lemma mkApps_tRel n a l : mkApps (tRel n) (a :: l) = tApp (tRel n) (a :: l).
+Proof.
+  simpl. reflexivity.
+Qed.
+
+Lemma lift_mkApps n k t l : lift n k (mkApps t l) = mkApps (lift n k t) (map (lift n k) l).
+Proof.
+  revert n k t; induction l; intros n k t; destruct t; try reflexivity.
+  rewrite lift_rel_alt. rewrite !mkApps_tRel.
+  simpl lift.
+  simpl map. rewrite !mkApps_tRel.
+  f_equal. destruct leb; auto.
+
+  simpl. f_equal.
+  now rewrite map_app.
+Qed.
+
 Lemma commut_lift_subst_rec :
   forall M N n p k,
     k <= p ->
@@ -293,6 +375,10 @@ Proof.
       now rewrite subst_rel_lt.
     + rewrite lift_rel_lt; try easy.
       now rewrite subst_rel_lt.
+
+  - rewrite lift_mkApps. f_equal. auto.
+    rewrite map_map_compose. apply_spec. intros.
+    now apply H2.
 Qed.
 
 Lemma commut_lift_subst :
@@ -300,7 +386,6 @@ Lemma commut_lift_subst :
   now intros; rewrite commut_lift_subst_rec.
 Qed.
 
-
 Lemma distr_lift_subst_rec :
   forall M N n p k,
     lift_rec n (subst_rec N M p) (p + k) =
@@ -333,6 +418,9 @@ Proof.
     + rewrite lift_rel_lt; try easy.
       now rewrite subst_rel_lt.
 
+  - rewrite lift_mkApps. f_equal; auto.
+    rewrite map_map_compose; apply_spec; simpl.
+    intros. apply H1.
   - rewrite add_assoc, H0. f_equal. now f_equal.
   - rewrite add_assoc, H0. f_equal. now f_equal.
 Qed.
@@ -347,9 +435,21 @@ Proof.
   apply distr_lift_subst_rec.
 Qed.
 
+Lemma mkApp_nested f l l' : mkApps (mkApps f l) l' = mkApps f (l ++ l').
+Proof.
+  induction l; destruct f; destruct l'; simpl; rewrite ?app_nil_r; auto.
+  f_equal. now rewrite <- app_assoc.
+Qed.
+
+Lemma subst_mkApps u k t l : subst u k (mkApps t l) = mkApps (subst u k t) (map (subst u k) l).
+Proof.
+  revert u k t; induction l; intros u k t; destruct t; try reflexivity.
+  intros. simpl mkApps at 1. simpl subst at 2. simpl subst at 1.
+  rewrite map_app. now rewrite mkApp_nested.
+Qed.
 
 Lemma distr_subst_rec :
-  forall M N (P : term) n p,
+  forall M N (P : term) (wfP : wf P) n p,
     subst_rec P (subst_rec N M p) (p + n) =
     subst_rec (subst_rec P N n) (subst_rec P M (S (p + n))) p.
 Proof.
@@ -383,18 +483,21 @@ Proof.
          now rewrite subst_rel_gt.
     + rewrite !subst_rel_lt; try easy.
 
-  - rewrite add_assoc, H0. f_equal. now f_equal.
-  - rewrite add_assoc, H0. f_equal. now f_equal.
+  - rewrite !subst_mkApps. rewrite H; auto. f_equal.
+    rewrite !map_map_compose. apply_spec. intros.
+    unfold compose. auto.
+  - rewrite add_assoc, H0; auto. f_equal. now f_equal.
+  - rewrite add_assoc, H0; auto. f_equal. now f_equal.
 Qed.
 
 Lemma distr_subst :
-  forall (P : term) N M k,
+  forall (P : term) (wfP : wf P) N M k,
     subst_rec P (subst0 N M) k = subst0 (subst_rec P N k) (subst_rec P M (S k)).
 Proof.
   intros; unfold subst in |- *.
   pattern k at 1 3 in |- *.
   change k with (0 + k).
-  apply distr_subst_rec.
+  now apply distr_subst_rec.
 Qed.
 
 
diff --git a/template-coq/theories/MetaTheory.v b/template-coq/theories/MetaTheory.v
new file mode 100644
index 000000000..bf57a4b95
--- /dev/null
+++ b/template-coq/theories/MetaTheory.v
@@ -0,0 +1,26 @@
+(* Distributed under the terms of the MIT license.   *)
+
+From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
+From Template Require Import config utils Ast univ Induction LiftSubst UnivSubst Typing.
+From Template Require AstUtils.
+Require Import String.
+Local Open Scope string_scope.
+Set Asymmetric Patterns.
+
+Existing Instance config.default_checker_flags.
+
+(** Use a coercion for this common projection of the global context. *)
+Definition fst_ctx : global_context -> global_declarations := fst.
+Coercion fst_ctx : global_context >-> global_declarations.
+
+(** The subject reduction property of the system: *)
+
+Conjecture subject_reduction : forall (Σ : global_context) Γ t u T,
+    Σ ;;; Γ |- t : T -> red Σ Γ t u -> Σ ;;; Γ |- u : T.
+
+(** Weak Normalization: every term has a normal form *)
+
+Definition normal (Σ : global_context) Γ t := ~ exists u, red1 Σ Γ t u.
+
+Conjecture weak_normalization : forall (Σ : global_context) Γ t T,
+    Σ ;;; Γ |- t : T -> exists u, red Σ Γ t u /\ normal Σ Γ u.
diff --git a/template-coq/theories/Retyping.v b/template-coq/theories/Retyping.v
new file mode 100644
index 000000000..6d7ac7c64
--- /dev/null
+++ b/template-coq/theories/Retyping.v
@@ -0,0 +1,122 @@
+(* Distributed under the terms of the MIT license.   *)
+
+From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
+From Template Require Import config monad_utils utils Ast univ Induction LiftSubst UnivSubst Typing Checker.
+From Template Require AstUtils.
+Require Import String.
+Local Open Scope string_scope.
+Set Asymmetric Patterns.
+Import monad_utils.MonadNotation.
+
+Existing Instance default_checker_flags.
+
+(** * Retyping
+
+  The [type_of] function provides a fast (and loose) type inference
+  function which assumes that the provided term is already well-typed in
+  the given context and recomputes its type. Only reduction (for
+  head-reducing types to uncover dependent products or inductives) and
+  substitution are costly here. No universe checking or conversion is done
+  in particular. *)
+
+Section TypeOf.
+  Context `{F : Fuel}.
+  Context (Σ : global_context).
+
+  Fixpoint infer_spine (Γ : context) (ty : term) (l : list term)
+           {struct l} : typing_result term :=
+    match l with
+    | nil => ret ty
+    | cons x xs =>
+      pi <- reduce_to_prod (fst Σ) Γ ty ;;
+         let '(a1, b1) := pi in
+         infer_spine Γ (subst0 x b1) xs
+    end.
+
+  Section SortOf.
+    Context (type_of : context -> term -> typing_result term).
+
+    Definition type_of_as_sort Γ t :=
+      tx <- type_of Γ t ;;
+      reduce_to_sort (fst Σ) Γ tx.
+
+  End SortOf.
+
+  Fixpoint type_of (Γ : context) (t : term) : typing_result term :=
+    match t with
+    | tRel n =>
+      match nth_error Γ n with
+      | Some d => ret (lift0 (S n) d.(decl_type))
+      | None => raise (UnboundRel n)
+      end
+
+    | tVar n => raise (UnboundVar n)
+    | tMeta n => raise (UnboundMeta n)
+    | tEvar ev args => raise (UnboundEvar ev)
+
+    | tSort s => ret (tSort (try_suc s))
+
+    | tCast c k t => ret t
+
+    | tProd n t b =>
+      s1 <- type_of_as_sort type_of Γ t ;;
+      s2 <- type_of_as_sort type_of (Γ ,, vass n t) b ;;
+      ret (tSort (Universe.sort_of_product s1 s2))
+
+    | tLambda n t b =>
+      t2 <- type_of (Γ ,, vass n t) b ;;
+       ret (tProd n t t2)
+
+    | tLetIn n b b_ty b' =>
+      b'_ty <- type_of (Γ ,, vdef n b b_ty) b' ;;
+      ret (tLetIn n b b_ty b'_ty)
+
+    | tApp t l =>
+      t_ty <- type_of Γ t ;;
+      infer_spine Γ t_ty l
+
+    | tConst cst u =>
+      tycstrs <- lookup_constant_type Σ cst u ;;
+      let '(ty, cstrs) := tycstrs in
+      ret ty
+
+    | tInd (mkInd ind i) u =>
+      tycstrs <- lookup_ind_type Σ ind i u;;
+      let '(ty, cstrs) := tycstrs in
+      ret ty
+
+    | tConstruct (mkInd ind i) k u =>
+      tycstrs <- lookup_constructor_type  Σ ind i k u ;;
+      let '(ty, cstrs) := tycstrs in
+      ret ty
+
+    | tCase (ind, par) p c brs =>
+      ty <- type_of Γ c ;;
+      indargs <- reduce_to_ind (fst Σ) Γ ty ;;
+      let '(ind', u, args) := indargs in
+      ret (tApp p (List.skipn par args ++ [c]))
+
+    | tProj p c =>
+      ty <- type_of Γ c ;;
+      indargs <- reduce_to_ind (fst Σ) Γ ty ;;
+      (* FIXME *)
+      ret ty
+
+    | tFix mfix n =>
+      match nth_error mfix n with
+      | Some f => ret f.(dtype)
+      | None => raise (IllFormedFix mfix n)
+      end
+
+    | tCoFix mfix n =>
+      match nth_error mfix n with
+      | Some f => ret f.(dtype)
+      | None => raise (IllFormedFix mfix n)
+      end
+    end.
+
+  Definition sort_of (Γ : context) (t : term) : typing_result universe :=
+    ty <- type_of Γ t;;
+    type_of_as_sort type_of Γ ty.
+
+End TypeOf.
\ No newline at end of file
diff --git a/template-coq/theories/Typing.v b/template-coq/theories/Typing.v
index e66ca0492..13da9fef1 100644
--- a/template-coq/theories/Typing.v
+++ b/template-coq/theories/Typing.v
@@ -946,14 +946,6 @@ Fixpoint globenv_size (Σ : global_declarations) : size :=
     - size of the global_context, including size of the global declarations in it
     - size of the derivation. *)
 
-(** Such a useful tactic it should be part of the stdlib. *)
-Ltac forward_gen H tac :=
-  match type of H with
-  | ?X -> _ => let H' := fresh in assert (H':X) ; [tac|specialize (H H'); clear H']
-  end.
-
-Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
-Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.
 Require Import Wf.
 
 (** Define non-dependent lexicographic products *)
diff --git a/template-coq/theories/WcbvEval.v b/template-coq/theories/WcbvEval.v
new file mode 100644
index 000000000..08284390b
--- /dev/null
+++ b/template-coq/theories/WcbvEval.v
@@ -0,0 +1,278 @@
+(* Distributed under the terms of the MIT license.   *)
+
+From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
+From Template Require Import config utils Ast univ Induction LiftSubst UnivSubst Typing.
+From Template Require AstUtils.
+Require Import String.
+Local Open Scope string_scope.
+Set Asymmetric Patterns.
+
+Existing Instance default_checker_flags.
+
+(** * Weak (head) call-by-value evaluation strategy.
+
+  The [wcbveval] inductive relation specifies weak cbv evaluation.  It
+  is shown to be a subrelation of the 1-step reduction relation from
+  which conversion is defined. Hence two terms that reduce to the same
+  wcbv head normal form are convertible.
+
+  This reduction strategy is supposed to mimick at the Coq level the
+  reduction strategy of ML programming languages. It is used to state
+  the extraction conjecture that can be applied to Coq terms to produce
+  (untyped) terms where all proofs are erased to a dummy value. *)
+
+(** ** Big step version of weak cbv beta-zeta-iota-fix-delta reduction.
+
+  TODO: CoFixpoints *)
+
+Section Wcbv.
+  Context (Σ : global_declarations) (Γ : context).
+  (* The local context is fixed: we are only doing weak reductions *)
+
+  Inductive eval : term -> term -> Prop :=
+  (** Reductions *)
+  (** Beta *)
+  | eval_beta f na t b a a' l res :
+      eval f (tLambda na t b) ->
+      eval a a' ->
+      eval (mkApps (subst0 a' b) l) res ->
+      eval (tApp f (a :: l)) res
+
+  (** Let *)
+  | eval_zeta na b0 b0' t b1 res :
+      eval b0 b0' ->
+      eval (subst0 b0' b1) res ->
+      eval (tLetIn na b0 t b1) res
+
+  (** Local variables: defined or undefined *)
+  | eval_rel_def i (isdecl : i < List.length Γ) body res :
+      (safe_nth Γ (exist _ i isdecl)).(decl_body) = Some body ->
+      eval (lift0 (S i) body) res ->
+      eval (tRel i) res
+
+  | eval_rel_undef i (isdecl : i < List.length Γ) :
+      (safe_nth Γ (exist _ i isdecl)).(decl_body) = None ->
+      eval (tRel i) (tRel i)
+
+  (** Case *)
+  | eval_iota ind pars discr c u args p brs res :
+      eval discr (mkApps (tConstruct ind c u) args) ->
+      eval (iota_red pars c args brs) res ->
+      eval (tCase (ind, pars) p discr brs) res
+
+  (** Fix unfolding, with guard *)
+  | eval_fix mfix idx args args' narg fn res :
+      unfold_fix mfix idx = Some (narg, fn) ->
+      Forall2 eval args args' -> (* FIXME should we reduce the args after the recursive arg here? *)
+      is_constructor narg args' = true ->
+      eval (mkApps fn args') res ->
+      eval (tApp (tFix mfix idx) args) res
+
+  (** Constant unfolding *)
+  | eval_delta c decl body (isdecl : declared_constant Σ c decl) u res :
+      decl.(cst_body) = Some body ->
+      eval (subst_instance_constr u body) res ->
+      eval (tConst c u) res
+
+  (** Proj *)
+  | eval_proj i pars arg discr args k u res :
+      eval discr (mkApps (tConstruct i k u) args) ->
+      eval (List.nth (pars + arg) args tDummy) res ->
+      eval (tProj (i, pars, arg) discr) res
+
+  (* TODO CoFix *)
+  | eval_abs na M N : eval (tLambda na M N) (tLambda na M N)
+
+  | eval_prod na b t b' t' :
+      eval b b' -> eval t t' -> eval (tProd na b t) (tProd na b' t')
+
+  | eval_ind_ i u : eval (tInd i u) (tInd i u)
+
+  | eval_app_ind t i u l l' : l <> nil ->
+      eval t (tInd i u) ->
+      Forall2 eval l l' ->
+      eval (tApp t l) (tApp (tInd i u) l')
+
+  | eval_constr i k u :
+      eval (tConstruct i k u) (tConstruct i k u)
+
+  | eval_app_constr f i k u l l' : l <> nil ->
+      eval f (tConstruct i k u) ->
+      Forall2 eval l l' ->
+      eval (tApp f l) (tApp (tConstruct i k u) l')
+
+  (* | evar ev l l' : evals l l' -> eval (tEvar ev l) (tEvar ev l') *)
+  | eval_evar ev l : eval (tEvar ev l) (tEvar ev l) (* Lets say it is a value for now *)
+
+  | eval_cast M1 k M2 N1 : eval M1 N1 -> eval (tCast M1 k M2) N1.
+
+  (** The right induction principle for the nested [Forall] cases: *)
+
+  Lemma eval_evals_ind :
+    forall P : term -> term -> Prop,
+      (forall (f : term) (na : name) (t b a a' : term) (l : list term) (res : term),
+          eval f (tLambda na t b) ->
+          P f (tLambda na t b) ->
+          eval a a' -> P a a' ->
+          eval (mkApps (b {0 := a'}) l) res -> P (mkApps (b {0 := a'}) l) res -> P (tApp f (a :: l)) res) ->
+
+      (forall (na : name) (b0 b0' t b1 res : term),
+          eval b0 b0' -> P b0 b0' -> eval (b1 {0 := b0'}) res -> P (b1 {0 := b0'}) res -> P (tLetIn na b0 t b1) res) ->
+
+      (forall (i : nat) (isdecl : i < #|Γ|) (body res : term),
+          decl_body (safe_nth Γ (exist (fun n : nat => n < #|Γ|) i isdecl)) = Some body ->
+          eval ((lift0 (S i)) body) res -> P ((lift0 (S i)) body) res -> P (tRel i) res) ->
+
+      (forall (i : nat) (isdecl : i < #|Γ|),
+          decl_body (safe_nth Γ (exist (fun n : nat => n < #|Γ|) i isdecl)) = None -> P (tRel i) (tRel i)) ->
+
+      (forall (ind : inductive) (pars : nat) (discr : term) (c : nat) (u : universe_instance)
+              (args : list term) (p : term) (brs : list (nat * term)) (res : term),
+          eval discr (mkApps (tConstruct ind c u) args) ->
+          P discr (mkApps (tConstruct ind c u) args) ->
+          eval (iota_red pars c args brs) res ->
+          P (iota_red pars c args brs) res -> P (tCase (ind, pars) p discr brs) res) ->
+
+      (forall (mfix : mfixpoint term) (idx : nat) (args args' : list term) (narg : nat) (fn res : term),
+          unfold_fix mfix idx = Some (narg, fn) ->
+          Forall2 eval args args' ->
+          Forall2 P args args' ->
+          is_constructor narg args' = true ->
+          eval (mkApps fn args') res -> P (mkApps fn args') res -> P (tApp (tFix mfix idx) args) res) ->
+
+      (forall (c : ident) (decl : constant_body) (body : term),
+          declared_constant Σ c decl ->
+          forall (u : universe_instance) (res : term),
+            cst_body decl = Some body ->
+            eval (subst_instance_constr u body) res -> P (subst_instance_constr u body) res -> P (tConst c u) res) ->
+
+      (forall (i : inductive) (pars arg : nat) (discr : term) (args : list term) (k : nat)
+              (u : universe_instance) (res : term),
+          eval discr (mkApps (tConstruct i k u) args) ->
+          P discr (mkApps (tConstruct i k u) args) ->
+          eval (nth (pars + arg) args tDummy) res ->
+          P (nth (pars + arg) args tDummy) res -> P (tProj (i, pars, arg) discr) res) ->
+
+      (forall (na : name) (M N : term), P (tLambda na M N) (tLambda na M N)) ->
+
+      (forall (na : name) (M M' N N' : term),
+          eval M M' -> eval N N' -> P M M' -> P N N' ->
+          P (tProd na M N) (tProd na M' N')) ->
+
+      (forall i u, P (tInd i u) (tInd i u)) ->
+
+      (forall (f8 : term) (i : inductive) (u : universe_instance) (l l' : list term),
+          l <> nil -> eval f8 (tInd i u) ->
+          P f8 (tInd i u) -> Forall2 eval l l' -> Forall2 P l l' -> P (tApp f8 l) (tApp (tInd i u) l')) ->
+
+      (forall i k u, P (tConstruct i k u) (tConstruct i k u)) ->
+
+      (forall (f8 : term) (i : inductive) (k : nat) (u : universe_instance) (l l' : list term),
+          l <> nil -> eval f8 (tConstruct i k u) ->
+          P f8 (tConstruct i k u) -> Forall2 eval l l' -> Forall2 P l l' -> P (tApp f8 l) (tApp (tConstruct i k u) l')) ->
+
+      (forall (ev : nat) (l : list term), P (tEvar ev l) (tEvar ev l)) ->
+
+      (forall (M1 : term) (k : cast_kind) (M2 N1 : term), eval M1 N1 -> P M1 N1 -> P (tCast M1 k M2) N1) ->
+
+      forall t t0 : term, eval t t0 -> P t t0.
+  Proof.
+    intros P Hbeta Hlet Hreldef Hrelvar Hcase Hfix Hconst Hproj Hlam Hprod Hind Hindapp Hcstr Hcstrapp Hevar Hcast.
+    fix 3. destruct 1;
+             try match goal with [ H : _ |- _ ] =>
+                             match type of H with
+                               forall t t0, eval t t0 -> _ => fail 1
+                             | _ => eapply H
+                             end end; eauto.
+    clear H1 H2.
+    revert args args' H0. fix aux 3. destruct 1. constructor; auto.
+    constructor. now apply eval_evals_ind. now apply aux.
+    revert l l' H H1. fix aux 4. destruct 2. contradiction. constructor.
+    now apply eval_evals_ind.
+    destruct l. inv H1; constructor.
+    now apply aux.
+    revert l l' H H1. fix aux 4. destruct 2. contradiction. constructor.
+    now apply eval_evals_ind. destruct l. inv H1; constructor. now apply aux.
+  Defined.
+
+  (** Characterization of values for this reduction relation:
+      Basically atoms (constructors, inductives, products (FIXME sorts missing))
+      and de Bruijn variables and lambda abstractions. Closed values disallow
+      de Bruijn variables. *)
+
+  Inductive value : term -> Prop :=
+  | value_tRel i : value (tRel i)
+  | value_tEvar ev l : value (tEvar ev l)
+  | value_tLam na t b : value (tLambda na t b)
+  | value_tProd na t u : value (tProd na t u)
+  | value_tInd i k l : List.Forall value l -> value (mkApps (tInd i k) l)
+  | value_tConstruct i k u l : List.Forall value l -> value (mkApps (tConstruct i k u) l).
+
+  Lemma value_values_ind : forall P : term -> Prop,
+       (forall i : nat, P (tRel i)) ->
+       (forall (ev : nat) (l : list term), P (tEvar ev l)) ->
+       (forall (na : name) (t b : term), P (tLambda na t b)) ->
+       (forall (na : name) (t u : term), P (tProd na t u)) ->
+       (forall (i : inductive) (k : universe_instance) l, List.Forall value l -> List.Forall P l -> P (mkApps (tInd i k) l)) ->
+       (forall (i : inductive) (k : nat) (u : universe_instance) (l : list term),
+        List.Forall value l -> List.Forall P l -> P (mkApps (tConstruct i k u) l)) -> forall t : term, value t -> P t.
+  Proof.
+    intros P ??????.
+    fix value_values_ind 2. destruct 1. 1-4:clear value_values_ind; auto.
+    apply H3. apply H5.
+    revert l H5. fix aux 2. destruct 1. constructor; auto.
+    constructor. now apply value_values_ind. now apply aux.
+    apply H4. apply H5.
+    revert l H5. fix aux 2. destruct 1. constructor; auto.
+    constructor. now apply value_values_ind. now apply aux.
+  Defined.
+
+  (** The codomain of evaluation is only values:
+      It means no redex can remain at the head of an evaluated term. *)
+
+  Lemma Forall2_right {A B} (P : B -> Prop) (l : list A) (l' : list B) :
+    Forall2 (fun x y => P y) l l' -> List.Forall (fun x => P x) l'.
+  Proof.
+    induction 1; constructor; auto.
+  Qed.
+
+  Lemma Forall2_non_nil {A B} (P : A -> B -> Prop) (l : list A) (l' : list B) :
+    Forall2 P l l' -> l <> nil -> l' <> nil.
+  Proof.
+    induction 1; congruence.
+  Qed.
+
+  Lemma eval_to_value e e' : eval e e' -> value e'.
+  Proof.
+    induction 1 using eval_evals_ind; simpl; auto using value.
+    eapply (value_tInd i u []); try constructor.
+    pose proof (value_tInd i u l'). forward H3.
+    apply (Forall2_right _ _ _ H2).
+    rewrite mkApps_tApp in H3; auto. simpl; auto. eauto using Forall2_non_nil.
+    eapply (value_tConstruct i k u []); try constructor.
+    pose proof (value_tConstruct i k u l'). forward H3.
+    apply (Forall2_right _ _ _ H2).
+    rewrite mkApps_tApp in H3; auto. simpl; auto. eauto using Forall2_non_nil.
+  Qed.
+
+  (** Evaluation preserves closedness: *)
+  Lemma eval_closed : forall n t u, closedn n t = true -> eval t u -> closedn n u = true.
+  Proof.
+    induction 2 using eval_evals_ind; simpl in *; eauto. eapply IHeval3.
+    admit.
+  Admitted. (* FIXME complete *)
+
+End Wcbv.
+
+(** Well-typed closed programs can't go wrong: they always evaluate to a value. *)
+
+Conjecture closed_typed_wcbeval : forall (Σ : global_context) t T,
+    Σ ;;; [] |- t : T -> exists u, eval (fst Σ) [] t u.
+
+(** Evaluation is a subrelation of reduction: *)
+
+Lemma wcbeval_red : forall (Σ : global_declarations) Γ t u,
+    eval Σ Γ t u -> red Σ Γ t u.
+Proof.
+  induction 1; try constructor; eauto.
+Admitted. (** TODO: Congruence lemmas of red for all constructions (as done in Coq in Coq) *)
diff --git a/template-coq/theories/monad_utils.v b/template-coq/theories/monad_utils.v
index de416307f..a8ebb4e93 100644
--- a/template-coq/theories/monad_utils.v
+++ b/template-coq/theories/monad_utils.v
@@ -57,32 +57,32 @@ End MapOpt.
 
 Section MonadOperations.
   Context {T} {M : Monad T}.
-
-  Fixpoint monad_map {A B} (f : A -> T B) (l : list A)
+  Context {A B} (f : A -> T B).
+  Fixpoint monad_map (l : list A)
     : T (list B)
     := match l with
        | nil => ret nil
        | x :: l => x' <- f x ;;
-                  l' <- monad_map f l ;;
+                  l' <- monad_map l ;;
                   ret (x' :: l')
        end.
 
-  Fixpoint monad_fold_left {A B} (f : A -> B -> T A) (l : list B) (x : A)
-    : T A
+  Context (g : A -> B -> T A).
+  Fixpoint monad_fold_left (l : list B) (x : A) : T A
     := match l with
        | nil => ret x
-       | y :: l => x' <- f x y ;;
-                     monad_fold_left f l x'
+       | y :: l => x' <- g x y ;;
+                   monad_fold_left l x'
        end.
 
-
-  Fixpoint monad_map_i_aux {A B} (f : nat -> A -> T B) (n0 : nat) (l : list A) : T (list B)
+  Context (h : nat -> A -> T B).
+  Fixpoint monad_map_i_aux (n0 : nat) (l : list A) : T (list B)
     := match l with
        | nil => ret nil
-       | x :: l => x' <- (f n0 x) ;;
-                     l' <- (monad_map_i_aux f (S n0) l) ;;
-                     ret (x' :: l')
+       | x :: l => x' <- (h n0 x) ;;
+                   l' <- (monad_map_i_aux (S n0) l) ;;
+                   ret (x' :: l')
        end.
 
-  Definition monad_map_i {A B} f := @monad_map_i_aux A B f 0.
+  Definition monad_map_i := @monad_map_i_aux 0.
 End MonadOperations.
diff --git a/template-coq/theories/utils.v b/template-coq/theories/utils.v
index f51ed4f8a..96c9c3803 100644
--- a/template-coq/theories/utils.v
+++ b/template-coq/theories/utils.v
@@ -2,6 +2,17 @@ From Coq Require Import Bool Program List String.
 Import ListNotations.
 Open Scope string_scope.
 
+Class Fuel := { fuel : nat }.
+
+(** Such a useful tactic it should be part of the stdlib. *)
+Ltac forward_gen H tac :=
+  match type of H with
+  | ?X -> _ => let H' := fresh in assert (H':X) ; [tac|specialize (H H'); clear H']
+  end.
+
+Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
+Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.
+
 Record squash (A : Type) : Prop := { _ : A }.
 
 Definition string_of_nat n :=