diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..28798520812627f93e02d5636b4c4645f06a3a89
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,242 @@
+#############################################################################
+## v # The Coq Proof Assistant ##
+## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
+## \VV/ # ##
+## // # Makefile automagically generated by coq_makefile V8.4pl3 ##
+#############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile lib/recdom/ core_lang.v iris.v lang.v masks.v world_prop.v -R lib/recdom/ RecDom
+#
+
+.DEFAULT_GOAL := all
+
+#
+# This Makefile may take arguments passed as environment variables:
+# COQBIN to specify the directory where Coq binaries resides;
+# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
+# DSTROOT to specify a prefix to install path.
+
+# Here is a hack to make $(eval $(shell works:
+define donewline
+
+
+endef
+includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
+$(call includecmdwithout@,$(COQBIN)coqtop -config)
+
+##########################
+# #
+# Libraries definitions. #
+# #
+##########################
+
+COQLIBS?=-I . -R lib/recdom/ RecDom
+COQDOCLIBS?=-R lib/recdom/ RecDom
+
+##########################
+# #
+# Variables definitions. #
+# #
+##########################
+
+
+OPT?=
+COQDEP?=$(COQBIN)coqdep -c
+COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
+COQCHKFLAGS?=-silent -o
+COQDOCFLAGS?=-interpolate -utf8
+COQC?=$(COQBIN)coqc
+GALLINA?=$(COQBIN)gallina
+COQDOC?=$(COQBIN)coqdoc
+COQCHK?=$(COQBIN)coqchk
+
+##################
+# #
+# Install Paths. #
+# #
+##################
+
+ifdef USERINSTALL
+XDG_DATA_HOME?=$(HOME)/.local/share
+COQLIBINSTALL=$(XDG_DATA_HOME)/coq
+COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
+else
+COQLIBINSTALL=${COQLIB}user-contrib
+COQDOCINSTALL=${DOCDIR}user-contrib
+endif
+
+######################
+# #
+# Files dispatching. #
+# #
+######################
+
+VFILES:=core_lang.v\
+ iris.v\
+ lang.v\
+ masks.v\
+ world_prop.v
+
+-include $(addsuffix .d,$(VFILES))
+.SECONDARY: $(addsuffix .d,$(VFILES))
+
+VOFILES:=$(VFILES:.v=.vo)
+VOFILESINC=$(filter $(wildcard ./*),$(VOFILES))
+GLOBFILES:=$(VFILES:.v=.glob)
+VIFILES:=$(VFILES:.v=.vi)
+GFILES:=$(VFILES:.v=.g)
+HTMLFILES:=$(VFILES:.v=.html)
+GHTMLFILES:=$(VFILES:.v=.g.html)
+ifeq '$(HASNATDYNLINK)' 'true'
+HASNATDYNLINK_OR_EMPTY := yes
+else
+HASNATDYNLINK_OR_EMPTY :=
+endif
+
+#######################################
+# #
+# Definition of the toplevel targets. #
+# #
+#######################################
+
+all: ./lib/recdom/ $(VOFILES)
+
+spec: $(VIFILES)
+
+gallina: $(GFILES)
+
+html: $(GLOBFILES) $(VFILES)
+ - mkdir -p html
+ $(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
+
+gallinahtml: $(GLOBFILES) $(VFILES)
+ - mkdir -p html
+ $(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
+
+all.ps: $(VFILES)
+ $(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all-gal.ps: $(VFILES)
+ $(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all.pdf: $(VFILES)
+ $(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all-gal.pdf: $(VFILES)
+ $(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+validate: $(VOFILES)
+ $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
+
+beautify: $(VFILES:=.beautified)
+ 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: all opt byte archclean clean install userinstall depend html validate ./lib/recdom/
+
+###################
+# #
+# Subdirectories. #
+# #
+###################
+
+./lib/recdom/:
+ cd ./lib/recdom/ ; $(MAKE) all
+
+####################
+# #
+# Special targets. #
+# #
+####################
+
+byte:
+ $(MAKE) all "OPT:=-byte"
+
+opt:
+ $(MAKE) all "OPT:=-opt"
+
+userinstall:
+ +$(MAKE) USERINSTALL=true install
+
+install:
+ install -d $(DSTROOT)$(COQLIBINSTALL)/RecDom; \
+ for i in $(VOFILESINC); do \
+ install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/RecDom/`basename $$i`; \
+ done
+ (cd ./lib/recdom/; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/./lib/recdom/ install)
+
+install-doc:
+ install -d $(DSTROOT)$(COQDOCINSTALL)/RecDom/html
+ for i in html/*; do \
+ install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/RecDom/$$i;\
+ done
+
+clean:
+ rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
+ rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
+ - rm -rf html mlihtml
+ (cd ./lib/recdom/ ; $(MAKE) clean)
+
+archclean:
+ rm -f *.cmx *.o
+ (cd ./lib/recdom/ ; $(MAKE) archclean)
+
+printenv:
+ @$(COQBIN)coqtop -config
+ @echo CAMLC = $(CAMLC)
+ @echo CAMLOPTC = $(CAMLOPTC)
+ @echo PP = $(PP)
+ @echo COQFLAGS = $(COQFLAGS)
+ @echo COQLIBINSTALL = $(COQLIBINSTALL)
+ @echo COQDOCINSTALL = $(COQDOCINSTALL)
+
+###################
+# #
+# Implicit rules. #
+# #
+###################
+
+%.vo %.glob: %.v
+ $(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+%.vi: %.v
+ $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+
+%.g: %.v
+ $(GALLINA) $<
+
+%.tex: %.v
+ $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
+
+%.html: %.v %.glob
+ $(COQDOC) $(COQDOCFLAGS) -html $< -o $@
+
+%.g.tex: %.v
+ $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
+
+%.g.html: %.v %.glob
+ $(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@
+
+%.v.d: %.v
+ $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+%.v.beautified:
+ $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
diff --git a/iris.v b/iris.v
index 7a5ebdbdd7fd8152f1f941e2358da2a9132a5f7e..6d4ff9b4f4aa2aa225415eae84c6768155085e7b 100644
--- a/iris.v
+++ b/iris.v
@@ -1155,6 +1155,37 @@ Qed.
- simpl comp_list; now erewrite comm, pcm_op_unit by apply _.
Qed.
+ Program Definition cons_pred (φ : value -=> Prop): value -n> Props :=
+ n[(fun v => pcmconst (mkUPred (fun n r => φ v) _))].
+ Next Obligation.
+ firstorder.
+ Qed.
+ Next Obligation.
+ intros x y H_xy P n r. simpl. rewrite H_xy. tauto.
+ Qed.
+ Next Obligation.
+ intros x y H_xy P m r. simpl in H_xy. destruct n.
+ - intros LEZ. exfalso. omega.
+ - intros _. simpl. assert(H_xy': equiv x y) by assumption. rewrite H_xy'. tauto.
+ Qed.
+
+ Theorem soundness_obs m e (φ : value -=> Prop) n e' tp σ σ'
+ (HT : valid (ht m (ownS σ) e (cons_pred φ)))
+ (HSN : stepn n ([e], σ) (e' :: tp, σ'))
+ (HV : is_value e') :
+ φ (exist _ e' HV).
+ Proof.
+ edestruct (soundness _ _ _ _ _ 0 _ _ _ _ fdEmpty (ex_own _ σ, pcm_unit _) 1 HT HSN) as [w' [r' [s' [H_wle [H_phi _] ] ] ] ].
+ - simpl. hnf. exists (pcm_unit _).
+ rewrite pcm_op_unit by intuition. reflexivity.
+ - rewrite Plus.plus_comm. simpl. split.
+ + admit. (* TODO: rewrite comm. does not work though?? *)
+ + exists (fdEmpty (V:=res)). simpl. split; [reflexivity|].
+ intros i _. split; [tauto|].
+ intros _ _ [].
+ - exact H_phi.
+ Qed.
+
End Soundness.
Section HoareTripleProperties.