diff --git a/README.md b/README.md
index e3a5f58..865ab57 100644
--- a/README.md
+++ b/README.md
@@ -5,9 +5,10 @@ This is the Coq formalization of guarded interaction trees, associated examples
 ## Installation instructions
 
 To install the formalization you will need the Iris, std++, and Equations packages.
-The dependencies can be easily installed with the following commands:
+The dependencies can be easily installed using [Opam](https://opam.ocaml.org/) with the following commands:
 
 ```
+opam repo add coq-released https://coq.inria.fr/opam/released
 opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 opam update
 opam install . --deps-only
@@ -53,6 +54,7 @@ to the code structure.
     in `gitree/weakestpre.v`
   + The additional weakest precondition rules are in `program_logic.v`
     and `examples/store.v`
+  + The `iter` example is in `examples/iter.v`
 - **Section 7**
   + The logical relation and the adequacy proof are in `input_lang/logrel.v`
 - **Section 8**
@@ -68,7 +70,41 @@ to the code structure.
 
 ## Notes
 
+### Representations of binders
 For the representation of languages with binders, we follow the
 approach of (Benton, Hur, Kennedy, McBride, JAR 2012) with well-scoped
 terms and substitutions/renamings. 
 
+
+### Disjunction property
+Some results in the formalization make use of the disjunction property
+of Iris: if (P ∨ Q) is provable, then either P or Q are provable on
+their own. This propery is used to show safety of the weakest
+precondition, and it is related to the difference between internal and
+external reductions.
+
+The internal reductions of GITrees is the relation `istep`, as defined
+in the paper, and it has type `iProp` as it is an internal relatin.
+There is also a similar *external* reduction relation `sstep` which
+lives in Coq's `Prop`. We use the `istep` relation in our definitions
+(since it is an internal relation), but we want to state the safety
+result w.r.t. the external relation `sstep`, which we take to be the
+'proper definition' of the reductions for GITrees.
+
+Showing that `istep`-safety implies `sstep`-safety (i.e. that if a
+GITree can do an `istep` then it can also do a `sstep`) requires the
+disjunction propety. The disjunction property for Iris can be shown
+assuming classical axioms (e.g. LEM) on the `Prop`-level.
+
+In order not to introduce classical axioms into the whole
+formalization, we added the disjunction propety as an assumption to
+the safety theorem (`wp_safety`) and all of its instances (e.g. in
+logical relations).
+
+### Ground type of errors
+
+One other difference with the paper worth mentioning, is that in the
+formalization we "hardcode" the type `Err` of errors, whereas in the
+paper we leave it parameterized. That is why in the `affine_lang` case
+study we use `OtherError` to represent linearity violations, instead
+of `Err(Lin)`.
diff --git a/_CoqProject b/_CoqProject
index 2a72fbd..d9e9582 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -46,3 +46,4 @@ theories/examples/store.v
 theories/examples/pairs.v
 theories/examples/while.v
 theories/examples/factorial.v
+theories/examples/iter.v
diff --git a/theories/examples/iter.v b/theories/examples/iter.v
new file mode 100644
index 0000000..18ef4f9
--- /dev/null
+++ b/theories/examples/iter.v
@@ -0,0 +1,103 @@
+From gitrees Require Import prelude gitree.
+
+Section iter.
+  Context {E : opsInterp}.
+  Context {R} `{!Cofe R}.
+  Context `{!SubOfe natO R}.
+  Notation IT := (IT E R).
+  Notation ITV := (ITV E R).
+
+  Program Definition pre_iter_1 (itr : IT) : IT -n> IT -n> IT :=
+    λne f α, λit β, IF α (f ⊙ (itr ⊙ f ⊙ (NATOP Nat.sub α (Ret 1)) ⊙ β)) β.
+  Solve All Obligations with solve_proper_please.
+  Program Definition pre_iter_2 (itr : IT) : IT -n> IT :=
+    λne f, λit α, pre_iter_1 itr f α.
+  Solve All Obligations with solve_proper_please.
+  Program Definition pre_iter (itr : IT) : IT :=
+    λit f, pre_iter_2 itr f.
+    (* λit f α β, IF α (f ⊙ (itr ⊙ f ⊙ (NATOP Nat.sub α (Ret 1)) ⊙ β)) β. *)
+  Solve All Obligations with solve_proper_please.
+
+  #[local] Instance pre_iter_contractive : Contractive pre_iter.
+  Proof.
+    intro n.
+    repeat intro. unfold pre_iter.
+    repeat f_equiv. intro. simpl.
+    repeat f_equiv. intro. simpl.
+    f_equiv. apply Next_contractive.
+    destruct n.
+    { apply dist_later_0. }
+    apply dist_later_S.
+    apply dist_later_S in H. intro.
+    simpl. solve_proper.
+  Qed.
+  Definition ITER : IT := fixpoint pre_iter.
+
+  Lemma ITER_eq f α β `{!AsVal f, !AsVal α, !AsVal β}:
+    ITER ⊙ f ⊙ α ⊙ β ≡ Tick_n 3 $ IF α (f ⊙ (ITER ⊙ f ⊙ (NATOP Nat.sub α (Ret 1)) ⊙ β)) β.
+  Proof.
+    trans (pre_iter ITER ⊙ f ⊙ α ⊙ β).
+    - repeat f_equiv. apply (fixpoint_unfold pre_iter).
+    - trans (Tick (pre_iter_2 ITER f ⊙ α ⊙ β)).
+      { unfold pre_iter.
+        rewrite -APP'_Tick_l. do 2 f_equiv.
+        rewrite -APP'_Tick_l. do 2 f_equiv.
+        rewrite APP'_Fun_l. cbn-[pre_iter_2].
+        by rewrite Tick_eq. }
+      rewrite Tick_n_S. f_equiv.
+      trans (Tick (pre_iter_1 ITER f α ⊙ β)).
+      { unfold pre_iter_2.
+        rewrite -APP'_Tick_l. do 2 f_equiv.
+        rewrite APP'_Fun_l. cbn-[pre_iter_2].
+        by rewrite Tick_eq. }
+      rewrite Tick_n_S. f_equiv.
+      rewrite APP'_Fun_l. cbn.
+      by rewrite Tick_eq.
+  Qed.
+
+End iter.
+
+Section iter_wp.
+  Context {sz : nat}.
+  Variable (rs : gReifiers sz).
+  Context {R} `{!Cofe R}.
+  Context `{!SubOfe natO R}.
+  Notation F := (gReifiers_ops rs).
+  Notation IT := (IT F R).
+  Notation ITV := (ITV F R).
+  Context `{!invGS Σ, !stateG rs R Σ}.
+  Notation iProp := (iProp Σ).
+  Context {HCI : ∀ o : opid (sReifier_ops (gReifiers_sReifier rs)),
+             CtxIndep (gReifiers_sReifier rs)
+               (ITF_solution.IT (sReifier_ops (gReifiers_sReifier rs)) R) o}.
+
+  Lemma wp_iter f (m : nat) β Ψ `{!AsVal f} `{!NonExpansive Ψ} :
+    ⊢ WP@{rs} β {{ Ψ }} -∗
+      □ (∀ βv, Ψ βv -∗ WP@{rs} (f ⊙ (IT_of_V βv)) {{ Ψ }}) -∗
+      WP@{rs} (ITER ⊙ f ⊙ (Ret m) ⊙ β) {{ Ψ }}.
+  Proof using HCI.
+    iIntros "Hb #H".
+    iApply (wp_bind _ (AppRSCtx (ITER ⊙ f ⊙ (Ret m)))).
+    iApply (wp_wand with "Hb").
+    iIntros (βv) "Hb". iModIntro.
+    iLöb as "IH" forall (m βv).
+    unfold AppRSCtx. simpl.
+    rewrite ITER_eq. iApply wp_tick. iNext.
+    iApply wp_tick. iNext. iApply wp_tick. iNext.
+    destruct m as [|m].
+    { rewrite IF_False; last lia.
+      by iApply wp_val. }
+    rewrite IF_True; last lia.
+    iApply (wp_bind _ (AppRSCtx f)).
+    iAssert ((NATOP Nat.sub (Ret (S m)) (Ret 1)) ≡ (Ret m : IT))%I as "Heq".
+    { iPureIntro. rewrite (NATOP_Ret (S m) 1 Nat.sub). f_equiv.
+      rewrite Nat.sub_1_r. done. }
+    iRewrite "Heq".
+    iSpecialize ("IH" with "Hb").
+    iApply (wp_wand with "IH").
+    iIntros (β'v) "Hb". iModIntro.
+    unfold AppRSCtx.
+    by iApply "H".
+  Qed.
+
+End iter_wp.
diff --git a/theories/input_lang_callcc/hom.v b/theories/input_lang_callcc/hom.v
new file mode 100644
index 0000000..7250497
--- /dev/null
+++ b/theories/input_lang_callcc/hom.v
@@ -0,0 +1,130 @@
+From Equations Require Import Equations.
+From gitrees Require Import gitree.
+From gitrees.input_lang_callcc Require Import lang interp.
+Require Import gitrees.lang_generic_sem.
+Require Import Binding.Lib Binding.Set Binding.Env.
+
+Open Scope stdpp_scope.
+
+Section hom.
+  Context {sz : nat}.
+  Context {rs : gReifiers sz}.
+  Context {subR : subReifier reify_io rs}.
+  Notation F := (gReifiers_ops rs).
+  Notation IT := (IT F natO).
+  Notation ITV := (ITV F natO).
+
+  Definition HOM : ofe := @sigO (IT -n> IT) IT_hom.
+
+  Global Instance HOM_hom (κ : HOM) : IT_hom (`κ).
+  Proof.
+    apply (proj2_sig κ).
+  Qed.
+
+  Program Definition HOM_id : HOM := exist _ idfun _.
+  Next Obligation.
+    apply _.
+  Qed.
+
+  Lemma HOM_ccompose (f g : HOM) :
+    ∀ α, `f (`g α) = (`f ◎ `g) α.
+  Proof.
+    intro; reflexivity.
+  Qed.
+
+  Program Definition HOM_compose (f g : HOM) : HOM := exist _ (`f ◎ `g) _.
+  Next Obligation.
+    intros f g; simpl.
+    apply _.
+  Qed.
+
+  Lemma HOM_compose_ccompose (f g h : HOM) :
+    h = HOM_compose f g ->
+    `f ◎ `g = `h.
+  Proof. intros ->. done. Qed.
+
+  Program Definition IFSCtx_HOM α β : HOM := exist _ (λne x, IFSCtx α β x) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition NatOpRSCtx_HOM {S : Set} (op : nat_op)
+    (α : @interp_scope F natO _ S -n> IT) (env : @interp_scope F natO _ S)
+    : HOM := exist _ (interp_natoprk rs op α (λne env, idfun) env) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition NatOpLSCtx_HOM {S : Set} (op : nat_op)
+    (α : IT) (env : @interp_scope F natO _ S)
+    (Hv : AsVal α)
+    : HOM := exist _ (interp_natoplk rs op (λne env, idfun) (constO α) env) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition ThrowLSCtx_HOM {S : Set}
+    (α : @interp_scope F natO _ S -n> IT)
+    (env : @interp_scope F natO _ S)
+    : HOM := exist _ ((interp_throwlk rs (λne env, idfun) α env)) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition ThrowRSCtx_HOM {S : Set}
+    (β : IT) (env : @interp_scope F natO _ S)
+    (Hv : AsVal β)
+    : HOM := exist _ (interp_throwrk rs (constO β) (λne env, idfun) env) _.
+  Next Obligation.
+    intros; simpl.
+    simple refine (IT_HOM _ _ _ _ _); intros; simpl.
+    - solve_proper_please.
+    - destruct Hv as [? <-].
+      rewrite ->2 get_val_ITV.
+      simpl. by rewrite get_fun_tick.
+    - destruct Hv as [x Hv].
+      rewrite <- Hv.
+      rewrite -> get_val_ITV.
+      simpl.
+      rewrite get_fun_vis.
+      repeat f_equiv.
+      intro; simpl.
+      rewrite <- Hv.
+      by rewrite -> get_val_ITV.
+    - destruct Hv as [? <-].
+      rewrite get_val_ITV.
+      simpl.
+      by rewrite get_fun_err.
+  Qed.
+
+  Program Definition OutputSCtx_HOM {S : Set}
+    (env : @interp_scope F natO _ S)
+    : HOM := exist _ ((interp_outputk rs (λne env, idfun) env)) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition AppRSCtx_HOM {S : Set}
+    (α : @interp_scope F natO _ S -n> IT)
+    (env : @interp_scope F natO _ S)
+    : HOM := exist _ (interp_apprk rs α (λne env, idfun) env) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+  Program Definition AppLSCtx_HOM {S : Set}
+    (β : IT) (env : @interp_scope F natO _ S)
+    (Hv : AsVal β)
+    : HOM := exist _ (interp_applk rs (λne env, idfun) (constO β) env) _.
+  Next Obligation.
+    intros; simpl.
+    apply _.
+  Qed.
+
+End hom.
diff --git a/theories/input_lang_callcc/logrel.v b/theories/input_lang_callcc/logrel.v
index 98bb695..db33e0b 100644
--- a/theories/input_lang_callcc/logrel.v
+++ b/theories/input_lang_callcc/logrel.v
@@ -1,7 +1,7 @@
 (** Logical relation for adequacy for the IO lang *)
 From Equations Require Import Equations.
 From gitrees Require Import gitree.
-From gitrees.input_lang_callcc Require Import lang interp.
+From gitrees.input_lang_callcc Require Import lang interp hom.
 Require Import gitrees.lang_generic_sem.
 Require Import Binding.Lib Binding.Set Binding.Env.
 
@@ -39,13 +39,6 @@ Section logrel.
         WP α {{ βv, ∃ m v σ', ⌜prim_steps e σ (Val v) σ' m⌝
                               ∗ logrel_nat βv v ∗ has_substate σ' }})%I.
 
-  Definition HOM : ofe := @sigO (IT -n> IT) IT_hom.
-
-  Global Instance HOM_hom (κ : HOM) : IT_hom (`κ).
-  Proof.
-    apply (proj2_sig κ).
-  Qed.
-
   Definition logrel_ectx {S} V (κ : HOM) (K : ectx S) : iProp :=
     (□ ∀ (βv : ITV) (v : val S), V βv v -∗ obs_ref (`κ (IT_of_V βv)) (fill K (Val v)))%I.
 
@@ -203,23 +196,6 @@ Section logrel.
     eapply Ectx_step; last apply Hpure; done.
   Qed.
 
-  Lemma HOM_ccompose (f g : HOM) :
-    ∀ α, `f (`g α) = (`f ◎ `g) α.
-  Proof.
-    intro; reflexivity.
-  Qed.
-
-  Program Definition HOM_compose (f g : HOM) : HOM := exist _ (`f ◎ `g) _.
-  Next Obligation.
-    intros f g; simpl.
-    apply _.
-  Qed.
-
-  Lemma HOM_compose_ccompose (f g h : HOM) :
-    h = HOM_compose f g ->
-    `f ◎ `g = `h.
-  Proof. intros ->. done. Qed.
-
   Lemma obs_ref_bind {S} (f : HOM) (K : ectx S) e α τ1 :
     ⊢ logrel τ1 α e -∗
       logrel_ectx (logrel_val τ1) f K -∗
@@ -307,12 +283,6 @@ Section logrel.
       apply BetaS.
   Qed.
 
-  Program Definition IFSCtx_HOM α β : HOM := exist _ (λne x, IFSCtx α β x) _.
-  Next Obligation.
-    intros; simpl.
-    apply _.
-  Qed.
-
   Lemma compat_if {S : Set} (Γ : S -> ty) (e0 e1 e2 : expr S) α0 α1 α2 τ :
     ⊢ logrel_valid Γ e0 α0  Tnat -∗
       logrel_valid Γ e1 α1 τ -∗
@@ -389,23 +359,6 @@ Section logrel.
     by constructor.
   Qed.
 
-  Program Definition NatOpRSCtx_HOM {S : Set} (op : nat_op)
-    (α : @interp_scope F natO _ S -n> IT) (env : @interp_scope F natO _ S)
-    : HOM := exist _ (interp_natoprk rs op α (λne env, idfun) env) _.
-  Next Obligation.
-    intros; simpl.
-    apply _.
-  Qed.
-
-  Program Definition NatOpLSCtx_HOM {S : Set} (op : nat_op)
-    (α : IT) (env : @interp_scope F natO _ S)
-    (Hv : AsVal α)
-    : HOM := exist _ (interp_natoplk rs op (λne env, idfun) (constO α) env) _.
-  Next Obligation.
-    intros; simpl.
-    apply _.
-  Qed.
-
   Lemma compat_natop {S : Set} (Γ : S -> ty) e1 e2 α1 α2 op :
     ⊢ logrel_valid Γ e1 α1 Tnat -∗
       logrel_valid Γ e2 α2 Tnat -∗
@@ -453,42 +406,6 @@ Section logrel.
     + intros. by constructor.
   Qed.
 
-  Program Definition ThrowLSCtx_HOM {S : Set}
-    (α : @interp_scope F natO _ S -n> IT)
-    (env : @interp_scope F natO _ S)
-    : HOM := exist _ ((interp_throwlk rs (λne env, idfun) α env)) _.
-  Next Obligation.
-    intros; simpl.
-    apply _.
-  Qed.
-
-  Program Definition ThrowRSCtx_HOM {S : Set}
-    (β : IT) (env : @interp_scope F natO _ S)
-    (Hv : AsVal β)
-    : HOM := exist _ (interp_throwrk rs (constO β) (λne env, idfun) env) _.
-  Next Obligation.
-    intros; simpl.
-    simple refine (IT_HOM _ _ _ _ _); intros; simpl.
-    - solve_proper_please.
-    - destruct Hv as [? <-].
-      rewrite ->2 get_val_ITV.
-      simpl. by rewrite get_fun_tick.
-    - destruct Hv as [x Hv].
-      rewrite <- Hv.
-      rewrite -> get_val_ITV.
-      simpl.
-      rewrite get_fun_vis.
-      repeat f_equiv.
-      intro; simpl.
-      rewrite <- Hv.
-      by rewrite -> get_val_ITV.
-    - destruct Hv as [? <-].
-      rewrite get_val_ITV.
-      simpl.
-      by rewrite get_fun_err.
-  Qed.
-
-
   Lemma compat_throw {S : Set} (Γ : S -> ty) τ τ' α β e e' :
     ⊢ logrel_valid Γ e α τ -∗
       logrel_valid Γ e' β (Tcont τ) -∗
@@ -512,7 +429,7 @@ Section logrel.
     simpl.
     rewrite get_val_ITV' -!fill_comp.
     simpl.
-    pose (κ'' := @ThrowRSCtx_HOM S (IT_of_V βv) ss _).
+    pose (κ'' := ThrowRSCtx_HOM (IT_of_V βv) ss _).
     (* TODO: some typeclasses bs *)
     assert ((get_fun (λne f : laterO (IT -n> IT), THROW (IT_of_V βv) f) (β ss)) ≡
               ((`κ'') (β ss))) as ->.
@@ -551,7 +468,7 @@ Section logrel.
     term_simpl.
     eapply prim_step_steps.
     eapply Throw_step; last done.
-    rewrite H. by rewrite -!fill_comp. 
+    rewrite H. by rewrite -!fill_comp.
   Qed.
 
 
@@ -620,14 +537,6 @@ Section logrel.
     constructor.
   Qed.
 
-  Program Definition OutputSCtx_HOM {S : Set}
-    (env : @interp_scope F natO _ S)
-    : HOM := exist _ ((interp_outputk rs (λne env, idfun) env)) _.
-  Next Obligation.
-    intros; simpl.
-    apply _.
-  Qed.
-
   Lemma compat_output {S} Γ (e: expr S) α :
     ⊢ logrel_valid Γ e α Tnat -∗
       logrel_valid Γ (Output e) (interp_output rs α) Tnat.
@@ -667,25 +576,6 @@ Section logrel.
     by constructor.
   Qed.
 
-
-  Program Definition AppRSCtx_HOM {S : Set}
-    (α : @interp_scope F natO _ S -n> IT)
-    (env : @interp_scope F natO _ S)
-    : HOM := exist _ (interp_apprk rs α (λne env, idfun) env) _.
-  Next Obligation.
-    intros; simpl.
-    apply _.
-  Qed.
-
-  Program Definition AppLSCtx_HOM {S : Set}
-    (β : IT) (env : @interp_scope F natO _ S)
-    (Hv : AsVal β)
-    : HOM := exist _ (interp_applk rs (λne env, idfun) (constO β) env) _.
-  Next Obligation.
-    intros; simpl.
-    apply _.
-  Qed.
-
   Lemma compat_app {S} Γ (e1 e2 : expr S) τ1 τ2 α1 α2 :
   ⊢ logrel_valid Γ e1 α1 (Tarr τ1 τ2) -∗
     logrel_valid Γ e2 α2 τ1 -∗
@@ -739,7 +629,20 @@ Section logrel.
     iApply "HV'"; iApply "HK".
   Qed.
 
-  (* TODO: finish throw + refactor *)
+  Lemma compat_nat {S : Set} (Γ : S -> ty) n :
+    ⊢ logrel_valid Γ (# n)%syn (interp_val rs (# n)%syn) ℕ%typ.
+  Proof.
+    iIntros (ss γ). iModIntro. iIntros "#Hss".
+    term_simpl.
+    iIntros (κ K) "#HK".
+    iSpecialize ("HK" $! (RetV n) (LitV n)).
+    rewrite IT_of_V_Ret.
+    iApply "HK".
+    simpl.
+    unfold logrel_nat.
+    iExists n; eauto.
+  Qed.
+
   Lemma fundamental {S : Set} (Γ : S -> ty) τ e :
     typed Γ e τ → ⊢ logrel_valid Γ e (interp_expr rs e) τ
   with fundamental_val {S : Set} (Γ : S -> ty) τ v :
@@ -768,15 +671,7 @@ Section logrel.
       + iApply compat_callcc.
         iApply IHtyped.
     - induction 1; simpl.
-      + iIntros (ss γ). iModIntro. iIntros "#Hss".
-        term_simpl.
-        iIntros (κ K) "#HK".
-        iSpecialize ("HK" $! (RetV n) (LitV n)).
-        rewrite IT_of_V_Ret.
-        iApply "HK".
-        simpl.
-        unfold logrel_nat.
-        iExists n; eauto.
+      + iApply compat_nat.
       + iApply compat_recV. by iApply fundamental.
   Qed.
 
@@ -852,9 +747,7 @@ Proof.
       intros Heq.
       rewrite (eq_pi _ _ Heq eq_refl)//.
     }
-    unshelve epose (idHOM := _ : (HOM rs)).
-    { exists idfun. apply IT_hom_idfun. }
-    iSpecialize ("Hlog" $! idHOM EmptyK with "[]").
+    iSpecialize ("Hlog" $! HOM_id EmptyK with "[]").
     {
       iIntros (βv v); iModIntro. iIntros "Hv". iIntros (σ'') "HS".
       iApply wp_val.