From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation lang.
From iris.program_logic Require Export atomic.

From iris.algebra Require Import cmra agree auth excl.

Section test.

  Definition za := (authR (prodUR
                             (prodUR
                                (optionUR (exclR unitO))
                                (optionUR (exclR unitO)))
                             (optionUR (agreeR (boolO))))).

  Class kkG Σ := Kk { kk_sG :> inG Σ za }.
  Definition kkΣ : gFunctors := #[GFunctor za].

  Instance subG_kkΣ {Σ} : subG kkΣ Σ -> kkG Σ.
  Proof. solve_inG. Qed.

  Context `{heapG Σ} `{kkG Σ}.
  Global Instance passed_persistent γ: Persistent (own γ (◯((None, None), Some (to_agree true)))).
  Proof. typeclasses eauto 10. Qed.