diff --git a/iris_check.v b/iris_check.v
index 236ec9d00bbc8937a09cc126bc8a146f3c4ae052..46af6c78a6de391398ca35f77add815d60ee8326 100644
--- a/iris_check.v
+++ b/iris_check.v
@@ -10,94 +10,17 @@ Set Bullet Behavior "Strict Subproofs".
 
 Module StupidLang : CORE_LANG.
   Inductive exprI :=
-  | unitI: exprI
-  | forkI: exprI -> exprI.
+  | unitI: exprI.
   Implicit Types (e: exprI).
   Definition expr := exprI.
-  Definition fork := forkI.
 
     
-  Definition is_value e := match e with
-                             | unitI => True
-                             | forkI _ => False
-                           end.
+  Definition is_value e := True.
   Definition value : Type := {e: expr | is_value e}.
   Definition is_value_dec e : is_value e + ~is_value e.
-    destruct e.
-    - left. exact I.
-    - right. tauto.
+    left. exact I.
   Defined.
 
-  Definition fork_ret := unitI.
-  Lemma fork_ret_is_value : is_value fork_ret.
-  Proof.
-    exact I.
-  Qed.
-  Definition fork_ret_val : value := exist _ fork_ret fork_ret_is_value.
-  Lemma fork_not_value e : ~is_value (fork e).
-  Proof.
-    tauto.
-  Qed.
-  Lemma fork_inj e1 e2: fork e1 = fork e2 -> e1 = e2.
-  Proof.
-    intros Heq. injection Heq. tauto.
-  Qed.
-
-  (** Evaluation contexts: You can just have the hole. There are no contexts below forks. **)
-  Definition ectx : Type := Datatypes.unit.
-  Implicit Types (K: ectx).
-  Definition empty_ctx := tt.
-  Definition comp_ctx K1 K2 := tt.
-  Definition fill K e := e.
-
-  Notation "'ε'"    := empty_ctx : lang_scope.
-  Notation "K1 ∘ K2"  := (comp_ctx K1 K2) (at level 40, left associativity) : lang_scope.
-  Notation "K '[[' e ']]' " := (fill K e) (at level 40, left associativity) : lang_scope.
-
-  Local Open Scope lang_scope.
-  
-  Lemma comp_ctx_assoc K0 K1 K2 : (K0 ∘ K1) ∘ K2 = K0 ∘ (K1 ∘ K2).
-  Proof. reflexivity. Qed.
-
-  Lemma comp_ctx_emp_r K : K ∘ ε = K.
-  Proof. destruct K. reflexivity. Qed.
-
-  Lemma comp_ctx_inj_r K K1 K2 : K ∘ K1 = K ∘ K2 -> K1 = K2.
-  Proof.
-    destruct K1, K2. now tauto.
-  Qed.
-
-  Lemma fill_empty e : ε [[ e ]] = e.
-  Proof.
-    reflexivity.
-  Qed.
-  Lemma fill_comp K1 K2 e :
-    K1 [[ K2 [[ e ]] ]] = K1 ∘ K2 [[ e ]].
-  Proof.
-    reflexivity.
-  Qed.
-  Lemma fill_inj_r K e1 e2 :
-    K [[ e1 ]] = K [[ e2 ]] -> e1 = e2.
-  Proof.
-    tauto.
-  Qed.
-  Lemma comp_ctx_positive K1 K2:
-    K1 ∘ K2 = ε -> K1 = ε /\ K2 = ε.
-  Proof.
-    destruct K1, K2. intros _. split; reflexivity.
-  Qed.
-  Lemma fill_value K e:
-    is_value (K [[ e ]]) -> is_value e.
-  Proof.
-    destruct K. now auto.
-  Qed.
-  Lemma fill_fork K e e':
-    fork e' = K [[ e ]] -> K = ε.
-  Proof.
-    destruct K. now auto.
-  Qed.
-    
-
   (** Shared machine state (e.g., the heap) **)
   Definition state : Type := Datatypes.unit.
   Implicit Types (σ: state).
@@ -106,67 +29,37 @@ Module StupidLang : CORE_LANG.
   Definition prim_cfg : Type := (expr * state)%type.
 
   (** The primitive atomic stepping relation **)
-  Definition prim_step (cfg1 cfg2: prim_cfg) := False.
-
+  Definition prim_step (cfg1 cfg2: prim_cfg) (ef: option expr) := False.
 
   Definition reducible e: Prop :=
-    exists sigma cfg', prim_step (e, sigma) cfg'.
+    exists sigma cfg' ef, prim_step (e, sigma) cfg' ef.
 
   Definition stuck (e : expr) : Prop :=
-    forall K e',
-      e = K [[ e' ]] ->
-      ~reducible e'.
+      ~reducible e.
 
-  Lemma fork_stuck K e:
-    stuck (K [[ fork e ]]).
-  Proof.
-    now firstorder.
-  Qed.
-  Lemma values_stuck e:
-    is_value e -> stuck e.
-  Proof.
-    now firstorder.
-  Qed.
+  (** Atomic expressions **)
+  Definition atomic e := False.
 
-  (* When something does a step, and another decomposition of the same
-     expression has a non-value e in the hole, then K is a left
-     sub-context of K' - in other words, e also contains the reducible
-     expression *)
-  Lemma step_by_value :
-    forall K K' e e',
-      K [[ e ]] = K' [[ e' ]] ->
-      reducible e' ->
-      ~ is_value e ->
-      exists K'', K' = K ∘ K''.
+  (** Properties *)
+  Lemma values_stuck :
+    forall e, is_value e -> stuck e.
   Proof.
-    now firstorder.
-  Qed.
-  (* Similar to above, buth with a fork instead of a reducible
-     expression *)
-  Lemma fork_by_value :
-    forall K K' e e',
-      K [[ e ]] = K' [[ fork e' ]] ->
-      ~ is_value e ->
-      exists K'', K' = K ∘ K''.
-  Proof.
-    intros. clear. destruct K, K'. exists ε. reflexivity.
+    firstorder.
   Qed.
 
-  (** Atomic expressions **)
-  Definition atomic e := False.
 
-  Lemma atomic_reducible :
-    forall e, atomic e -> reducible e.
+  Lemma atomic_not_value :
+    forall e, atomic e -> ~is_value e.
   Proof.
-    now firstorder.
+    firstorder.
   Qed.
 
-  Lemma atomic_step: forall e σ e' σ',
+  Lemma atomic_step: forall e σ e' σ' ef,
                        atomic e ->
-                       prim_step (e, σ) (e', σ') ->
+                       prim_step (e, σ) (e', σ') ef ->
                        is_value e'.
   Proof.
-    now firstorder.
+    firstorder.
   Qed.
 
 End StupidLang.
@@ -186,9 +79,9 @@ Module Res := IrisRes TrivialRA StupidLang.
 Module World := WorldProp Res.
 Module Import Core := IrisCore TrivialRA StupidLang Res World.
 Module Import Plog := IrisPlog TrivialRA StupidLang Res World Core.
-Module Import Meta := IrisMeta TrivialRA StupidLang Res World Core Plog.
 Module Import VSRules := IrisVSRules TrivialRA StupidLang Res World Core Plog.
 Module Import HTRules := IrisHTRules TrivialRA StupidLang Res World Core Plog.
+Module Import Meta := IrisMeta TrivialRA StupidLang Res World Core Plog HTRules.
 
 (* And now we check for axioms *)
 Print Assumptions adequacy_obs.