diff --git a/supplements/disj_correspondence.v b/supplements/disj_correspondence.v
new file mode 100644
index 0000000000000000000000000000000000000000..f33c0830ac75aa58b51a9b9fa46b064538848cf9
--- /dev/null
+++ b/supplements/disj_correspondence.v
@@ -0,0 +1,139 @@
+From diaframe Require Import proofmode_base.
+From iris.bi Require Import bi.
+From iris.proofmode Require Import proofmode.
+
+Goal True.
+(* R∧ *)
+(* is the result of composing two rules in the implementation: *)
+let lemma := open_constr:(solve_one_foc.tac_solve_one_foc_focus_solve_and _ id _ _ _ _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type.
+
+let lemma := open_constr:(solve_and.tac_solve_and _ _ _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type.
+
+(* R∨ *)
+let L1 := open_constr:(_) in
+let L2 := open_constr:(_) in
+let lemma := open_constr:(solve_one_foc.tac_solve_one_foc_fromor (TT := [tele]) _ id (L1 ∨ L2)%I L1 L2 _ L1 _ _ _ _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type.
+
+(* R-∗⊥ *)
+let lemma := open_constr:(introduce_hyp.tac_introduce_hyp_premise_pure _ False%I False _ true _ _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type. 
+(* combined with: *)
+Check False_ind.
+
+(* R-∗⊤ *)
+Check introduce_hyp.tac_introduce_hyp_premise_emp.
+
+(* R-∗∗ *)
+let U1 := open_constr:(_) in
+let U2 := open_constr:(_) in
+let lemma := open_constr:(introduce_hyp.tac_introduce_hyp_premise_sep _ (U1 ∗ U2)%I U1 U2 _ _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type.
+
+(* R-∗∨ *)
+let U1 := open_constr:(_) in
+let U2 := open_constr:(_) in
+let lemma := open_constr:(introduce_hyp.tac_introduce_hyp_premise_or _ (U1 ∨ U2)%I U1 U2 _ _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type. (* already internally applies R∧ *) 
+
+(* R-∗H*)
+let lemma := open_constr:(introduce_hyp.tac_introduce_hyp_merge_env _ _ _ _ _ _ None _ _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type.
+(* this still contains a match, since the hypothesis name [j] should be fresh *)
+
+(* R∗⊤ *)
+let L := open_constr:(_) in
+let D := open_constr:(_) in
+let lemma := open_constr:(solve_sep_foc.tac_solve_sep_foc_pure _ (TT := [tele]) false id ⊤ L D True (L ∨ D)%I _ _ _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type.
+
+(* R∗∗ *)
+let L1 := open_constr:(_) in
+let L2 := open_constr:(_) in
+let lemma := open_constr:(solve_sep_foc.tac_solve_sep_foc_from_sep (TT := [tele]) _ id (L1 ∗ L2)%I L1 L2 _ _ TeleO TeleO L1 TargO _ eq_refl _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type.
+
+(* R∗∨ *)
+let L1 := open_constr:(_) in
+let L2 := open_constr:(_) in
+let lemma := open_constr:(solve_sep_foc.tac_solve_sep_foc_fromdisj (TT := [tele]) _ id (L1 ∨ L2)%I L1 L1 L2 _ _ _ _ _ _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type.
+
+(* R∗A *)
+let H := open_constr:(_) in
+let A := open_constr:(_) in
+let L := open_constr:(_) in
+let U := open_constr:(_) in
+let Λ := open_constr:(_) in
+let G := open_constr:(_) in
+let Γ := open_constr:(_) in
+let lemma := open_constr:(solve_sep_foc.tac_solve_sep_foc_biabd_disj (TTl := [tele]) (TTr := [tele]) _ (Some _)
+  A L G U Γ (Some2 Λ) 
+  id false _ id id id id 
+  G Γ _
+) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type.
+
+(* unfocus *)
+let Γ := open_constr:(_) in
+let lemma := open_constr:(solve_sep_foc.tac_solve_sep_foc_unfocus (TT := [tele]) _ id _ _ Γ Γ _ _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn in lemma_type in
+idtac simpl_lemma_type.
+Abort.
+
+(* L-A *)
+Lemma L_A' {PROP : bi} (A : PROP) : BiAbdDisj (TTl :=[tele]) (TTr := [tele]) false A A id emp%I emp%I None2.
+Proof. apply _. Qed.
+
+Goal True.
+(* L∗ *)
+let U1 := open_constr:(_) in
+let U2 := open_constr:(_) in
+let lemma := open_constr:(lemmas_biabd_disj.biabd_disj_hyp_sepl (U1 ∗ U2)%I U1 U2 (TTl := [tele]) (TTr := [tele]) _ id _ _ (Some2 _) _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn -[BiAbdDisj] in lemma_type in
+idtac simpl_lemma_type.
+
+(* L-∗ *)
+let L1 := open_constr:(_) in
+let U1 := open_constr:(_) in
+let lemma := open_constr:(lemmas_biabd_disj.biabd_disj_hyp_wand false (L1 -∗ U1)%I L1 U1 (TTr := [tele]) (TTl := [tele]) _ id _ _ (Some2 _) _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn -[BiAbdDisj] in lemma_type in
+idtac simpl_lemma_type.
+
+(* L∨ *)
+let U1 := open_constr:(_) in
+let U2 := open_constr:(_) in
+let lemma := open_constr:(lemmas_biabd_disj.biabd_disj_hyp_orl (U1 ∨ U2)%I U1 U2 (TTl := [tele]) (TTr := [tele]) false _ id id _ _ (Some2 _) _) in
+let lemma_type := type of lemma in
+let simpl_lemma_type := eval cbn -[BiAbdDisj] in lemma_type in
+idtac simpl_lemma_type.
+Abort.
+
+
diff --git a/supplements/disj_simple_separation.v b/supplements/disj_simple_separation.v
index 9b9468021aa25ea00d93123799359de75524e328..af21739d67a5ab3fbcbbd627fdbcb20f90649ac7 100644
--- a/supplements/disj_simple_separation.v
+++ b/supplements/disj_simple_separation.v
@@ -4,19 +4,19 @@ From iris.proofmode Require Import proofmode.
 
 Section disj.
 Context {PROP : bi}. 
-(* Parametrized over general separation logics *)
-Context `{!BiAffine PROP}. 
-(* .. but affine separation logics, meaning we have P ⊢ emp. *)
+(* Parametrized over general separation logics, [bi]s in Iris lingo *)
 
 Implicit Types Δ Γ G U A : PROP.
 Notation "⊤" := emp%I.
 Notation "⊥" := False%I.
 
 (** Inversion phase *)
-Lemma R_top Δ Γ : Δ ⊢ ⊤ ∨ Γ.
+Lemma R_top Δ Γ `{!BiAffine PROP} : Δ ⊢ ⊤ ∨ Γ.
+(* This rule is only valid in _affine_ separation logics,
+  i.e. where we can discard resources: we have [P ⊢ ⊤] for all resources [P] *)
 Proof. iSteps. Qed.
 
-Lemma R_A Δ A Γ : 
+Lemma R_A Δ A Γ :
   (Δ ⊢ (A ∗ ⊤) ∨ Γ) →
   Δ ⊢ A ∨ Γ.
 Proof. move => ->. iSteps. Qed.
@@ -154,4 +154,16 @@ Proof.
   iSteps.
 Qed.
 
-End disj.
\ No newline at end of file
+End disj.
+
+
+
+
+
+
+
+
+
+
+
+