diff --git a/theories/prelude/classical.v b/theories/prelude/classical.v
new file mode 100644
index 0000000000000000000000000000000000000000..22ec16fcad057fc919943ec7f442f641b6c85891
--- /dev/null
+++ b/theories/prelude/classical.v
@@ -0,0 +1,103 @@
+(** * extensional model using ϵ, PE and FE *)
+From iris.prelude Require Export prelude.
+Require Import Coq.Logic.Epsilon.
+Require Import Coq.Logic.PropExtensionality.
+Require Import Coq.Logic.FunctionalExtensionality.
+Require Import Coq.Logic.Classical_Prop.
+
+(* some classical reasoning principles *)
+Lemma classic_or_to_sum (P Q : Prop) : P ∨ Q → P + Q.
+Proof.
+  intros HPQ. assert (exists (b : bool), if b then P else Q) as Hex.
+  { destruct HPQ; by [exists true|exists false]. }
+  apply constructive_indefinite_description in Hex as [[] ?]; eauto.
+Qed.
+
+Lemma classic_dn (X : Prop) : ¬ (¬ X) ↔ X.
+Proof.
+  destruct (classic X); tauto.
+Qed.
+
+Lemma classic_forall_exists_dn (X : Type) (P : X → Prop): (∀ x, P x) ↔ ¬ (∃ x, ¬ (P x)).
+Proof.
+  split.
+  - intros H (x & H1). eauto.
+  - intros H x. destruct (classic (P x)) as [| ?]; first done.
+    exfalso; apply H; eauto.
+Qed.
+
+Lemma classic_not_forall X (P: X → Prop): ¬ (∀ x: X, P x) ↔ ∃ x: X, ¬ P x.
+Proof.
+  by rewrite classic_forall_exists_dn classic_dn.
+Qed.
+
+Lemma classic_not_exists X (P: X → Prop): ¬ (∃ x: X, P x) ↔ ∀ x: X, ¬ P x.
+Proof.
+  by rewrite classic_forall_exists_dn; split; intros H [x ?]; eauto using classic_dn.
+Qed.
+
+Lemma classic_not_impl (P Q: Prop): ¬ (P → Q) ↔ P ∧ ¬ Q.
+Proof.
+  destruct (classic P); tauto.
+Qed.
+
+Lemma classic_find_least {X: Type} (R: X → X → Prop) (P: X → Prop) x:
+  wf R →
+  (∀ x y, R x y → P x → P y) →
+  P x →
+  ∃ y, P y ∧ ∀ x, R x y → ¬ P x.
+Proof.
+  intros Hwf HP. induction (Hwf x) as [x _ IH].
+  intros Hx. destruct (classic (∀ y, R y x → ¬ P y)) as [|Hn]; first by eauto.
+  revert Hn; rewrite classic_not_forall=> [[y]]; rewrite classic_not_impl classic_dn.
+  intros []; eauto.
+Qed.
+
+
+(* we use classical logic to define a normalizer function
+  for building quotients *)
+Section quotients.
+
+  Context {X: Type} (R: X → X → Prop) `{Equivalence X R}.
+  Definition norm (x: X) := epsilon (inhabits x) (R x).
+
+  Lemma rel_norm x y: R x y → norm x = norm y.
+  Proof.
+    intros HR; unfold norm; f_equal.
+    - apply proof_irrelevance.
+    - eapply functional_extensionality; intros u; eapply propositional_extensionality.
+      by rewrite HR.
+  Qed.
+
+  Lemma norm_pi s (Hq Hq': norm s = s): Hq = Hq'.
+  Proof.
+    apply proof_irrelevance.
+  Qed.
+
+  Lemma rel_norm_intro x: R x (norm x).
+  Proof.
+    unfold norm; eapply epsilon_spec; exists x; reflexivity.
+  Qed.
+
+  (* derived lemmas *)
+  Lemma norm_idem x: norm (norm x) = norm x.
+  Proof.
+    eapply rel_norm; symmetry; eapply rel_norm_intro.
+  Qed.
+
+  Lemma norm_rel x y: norm x = norm y → R x y.
+  Proof.
+    by intros Heq; rewrite (rel_norm_intro x) (rel_norm_intro y) Heq.
+  Qed.
+
+  Lemma norm_iff x y: norm x = norm y ↔ R x y.
+  Proof.
+    split; eauto using rel_norm, norm_rel.
+  Qed.
+
+  Global Instance norm_proper : Proper (R ==> R) norm.
+  Proof.
+    intros x y HR. by rewrite -(rel_norm_intro x) -(rel_norm_intro y).
+  Qed.
+
+End quotients.
\ No newline at end of file
diff --git a/theories/prelude/options.v b/theories/prelude/options.v
new file mode 100644
index 0000000000000000000000000000000000000000..cd6d5b0f3e04d341c94030c94e7fc240882a2122
--- /dev/null
+++ b/theories/prelude/options.v
@@ -0,0 +1,20 @@
+(** Coq configuration for Iris (not meant to leak to clients) *)
+(* Everything here should be [Export Set], which means when this
+file is *imported*, the option will only apply on the import site
+but not transitively. *)
+
+Export Set Default Proof Using "Type".
+Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)
+
+(* Enforces that every tactic is executed with a single focused goal, meaning
+that bullets and curly braces must be used to structure the proof. *)
+Export Set Default Goal Selector "!".
+
+(* We always annotate hints with locality ([Global] or [Local]). This enforces
+that at least global hints are annotated. *)
+Export Set Warnings "+deprecated-hint-without-locality".
+
+(* "Fake" import to whitelist this file for the check that ensures we import
+this file everywhere.
+From iris.prelude Require Import options.
+*)
diff --git a/theories/prelude/prelude.v b/theories/prelude/prelude.v
new file mode 100644
index 0000000000000000000000000000000000000000..f39e8a45fb9791b0c08b2d881486885bf2bb0348
--- /dev/null
+++ b/theories/prelude/prelude.v
@@ -0,0 +1,44 @@
+From Coq.ssr Require Export ssreflect.
+From stdpp Require Export prelude.
+From iris.prelude Require Import options.
+Global Open Scope general_if_scope.
+Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
+Ltac done := stdpp.tactics.done.
+
+
+(** Iris itself and many dependencies still rely on this coercion. *)
+Coercion Z.of_nat : nat >-> Z.
+
+
+
+
+(* some basic definitions and lemmas *)
+Inductive rc {A} (R: A → A → Prop) (x: A) (y: A):  Prop :=
+| rc_refl: x = y → rc R x y
+| rc_subrel: R x y → rc R x y.
+Global Hint Constructors rc : core.
+
+Global Instance rc_reflexive {A} (R : A → A → Prop) : Reflexive (rc R).
+Proof. intros ?; by apply rc_refl. Qed.
+Global Instance rc_subrelation {A} (R : A → A → Prop): subrelation R (rc R).
+Proof. intros ? ? ?; by apply rc_subrel. Qed.
+
+Lemma rc_iff {A} (R: A → A → Prop) x y: rc R x y ↔ R x y ∨ x = y.
+Proof.
+  split; destruct 1; eauto.
+Qed.
+
+Global Instance rc_transitive {A} (R: A → A → Prop) `{!Transitive R}: Transitive (rc R).
+Proof.
+  intros x y z [] []; subst; eauto.
+Qed.
+
+
+
+(* this is not classical, but useful *)
+Lemma ex_impl X (P: X → Prop) (Q: Prop): ((∃ x, P x) → Q) ↔ ∀ x, P x → Q.
+Proof.
+  split.
+  - intros H x Px; eapply H; by exists x.
+  - intros HPQ [x Px]; eauto.
+Qed.
\ No newline at end of file