Commit 71abda4d authored by Ralf Jung's avatar Ralf Jung
Browse files

make "make quick" quick by adding hints about the used section variables

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing
parent e0789039
Pipeline #3562 passed with stage
in 10 minutes and 49 seconds
From iris.algebra Require Export cmra.
From iris.algebra Require Import list.
From iris.base_logic Require Import base_logic.
(* FIXME: This file needs a 'Proof Using' hint. *)
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
......
From iris.algebra Require Export excl local_updates.
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import classes.
Set Default Proof Using "Type*".
Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
Add Printing Constructor auth.
......
From mathcomp Require Export ssreflect.
From iris.prelude Require Export prelude.
Set Default Proof Using "Type*".
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
Ltac done := prelude.tactics.done.
\ No newline at end of file
Ltac done := prelude.tactics.done.
From iris.algebra Require Export ofe.
Set Default Proof Using "Type*".
Class PCore (A : Type) := pcore : A option A.
Instance: Params (@pcore) 2.
......
From iris.algebra Require Export cmra list.
From iris.prelude Require Import functions gmap gmultiset.
Set Default Proof Using "Type*".
(** The operator [ [⋅] Ps ] folds [⋅] over the list [Ps]. This operator is not a
quantifier, so it binds strongly.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import cmra_big_op.
Set Default Proof Using "Type*".
(** * Simple solver for validity and inclusion by reflection *)
Module ra_reflection. Section ra_reflection.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From iris.prelude Require Export collections coPset.
Set Default Proof Using "Type*".
(** This is pretty much the same as algebra/gset, but I was not able to
generalize the construction without breaking canonical structures. *)
......
From iris.algebra Require Export ofe.
Set Default Proof Using "Type*".
Record solution (F : cFunctor) := Solution {
solution_car :> ofeT;
......
From iris.algebra Require Export cmra.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import local_updates.
Set Default Proof Using "Type*".
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_ /.
Local Arguments validN _ _ _ !_ /.
......
From iris.algebra Require Import ofe cmra.
Set Default Proof Using "Type*".
(* Old notation for backwards compatibility. *)
......
From iris.algebra Require Export cmra updates.
Set Default Proof Using "Type*".
Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
(* setoids *)
......
From iris.algebra Require Export cmra.
From iris.base_logic Require Import base_logic.
Set Default Proof Using "Type*".
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
......
From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra.
Set Default Proof Using "Type*".
Notation frac := Qp (only parsing).
......
......@@ -2,6 +2,7 @@ From iris.algebra Require Export cmra.
From iris.prelude Require Export gmap.
From iris.algebra Require Import updates local_updates.
From iris.base_logic Require Import base_logic.
Set Default Proof Using "Type*".
Section cofe.
Context `{Countable K} {A : ofeT}.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From iris.prelude Require Export collections gmap mapset.
Set Default Proof Using "Type*".
(* The union CMRA *)
Section gset.
......
From iris.algebra Require Export cmra.
From iris.base_logic Require Import base_logic.
From iris.prelude Require Import finite.
Set Default Proof Using "Type*".
(** * Indexed product *)
(** Need to put this in a definition to make canonical structures to work. *)
......
......@@ -2,6 +2,7 @@ From iris.algebra Require Export cmra.
From iris.prelude Require Export list.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import updates local_updates.
Set Default Proof Using "Type*".
Section cofe.
Context {A : ofeT}.
......
From iris.algebra Require Export cmra.
Set Default Proof Using "Type*".
(** * Local updates *)
Definition local_update {A : cmraT} (x y : A * A) := n mz,
......
From iris.algebra Require Export base.
Set Default Proof Using "Type*".
(** This files defines (a shallow embedding of) the category of OFEs:
Complete ordered families of equivalences. This is a cartesian closed
......
From iris.prelude Require Export set.
From iris.algebra Require Export cmra.
From iris.algebra Require Import dra.
Set Default Proof Using "Type*".
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments core _ _ !_ /.
......
  • Ralf Jung @jung

    mentioned in merge request !36 (closed)

    ·

    mentioned in merge request !36 (closed)

    Toggle commit list
  • Nice awk hacking :)

  • Yeah, took me a while ;-) . I also still don't understand why adding 1 at the end of the script makes it so that I don't lose the entire existing content of the file. Whatever,

  • Interestingly, there are some files where this has cost us a little performance... the overall user time is increased by 3sec (<0.5%), but this is pretty much entirely due to barrier/proof.v, algebra/list.v and algebra/sts.v which each got almost a second slower. Strange.

  • We may accidentally be parameterizing some definitions or lemmas by spurious type class arguments. Is there some way of figuring out where that happened?

    Edited by Robbert Krebbers
  • Alright, using SearchAbout _we can get a list of all definitions and lemmas. We should diff that between both commits.

  • Here's the diff:

    --- about-old   2017-01-04 12:14:09.494975041 +0100
    +++ about-new   2017-01-04 12:13:11.042545334 +0100
    @@ -33921,15 +33921,17 @@
       (Φ : val → uPred (iResUR Σ)),
       True -∗ ▷ (∀ l : loc, recv N l P ∗ send N l P -∗ Φ #l) -∗ WP newbarrier #() {{ v, Φ v }}
     ress_split:
    -  ∀ (Σ : gFunctors) (barrierG0 : barrierG Σ) (i i1 i2 : gname) (Q R1 R2 : ∙%CF (iProp Σ)) 
    -  (P : iProp Σ) (I : gset gname),
    -  i ∈ I
    -  → i1 ∉ I
    -    → i2 ∉ I
    -      → i1 ≠ i2
    -        → saved_prop_own i Q -∗
    -          saved_prop_own i1 R1 -∗
    -          saved_prop_own i2 R2 -∗ (Q -∗ R1 ∗ R2) -∗ ress P I -∗ ress P ({[i1; i2]} ∪ I ∖ {[i]})
    +  ∀ Σ : gFunctors,
    +  heapG Σ
    +  → ∀ (barrierG0 : barrierG Σ) (i i1 i2 : gname) (Q R1 R2 : ∙%CF (iProp Σ)) (P : iProp Σ) 
    +    (I : gset gname),
    +    i ∈ I
    +    → i1 ∉ I
    +      → i2 ∉ I
    +        → i1 ≠ i2
    +          → saved_prop_own i Q -∗
    +            saved_prop_own i1 R1 -∗
    +            saved_prop_own i2 R2 -∗ (Q -∗ R1 ∗ R2) -∗ ress P I -∗ ress P ({[i1; i2]} ∪ I ∖ {[i]})
     recv_ne:
       ∀ (Σ : gFunctors) (heapG0 : heapG Σ) (barrierG0 : barrierG Σ) (N : namespace) (n : nat) 
       (l : loc), Proper (dist n ==> dist n) (recv N l)
    @@ -33942,8 +33944,9 @@
     barrier_inv_ne:
       ∀ (Σ : gFunctors) (heapG0 : heapG Σ) (barrierG0 : barrierG Σ) (n : nat) (l : loc),
       Proper (dist n ==> eq ==> dist n) (barrier_inv l)
    -state_to_prop_ne: ∀ (Σ : gFunctors) (n : nat) (s : state), Proper (dist n ==> dist n) (state_to_prop s)
    -ress_ne: ∀ (Σ : gFunctors) (barrierG0 : barrierG Σ) (n : nat), Proper (dist n ==> eq ==> dist n) ress
    +state_to_prop_ne:
    +  ∀ Σ : gFunctors, heapG Σ → barrierG Σ → ∀ (n : nat) (s : state), Proper (dist n ==> dist n) (state_to_prop s)
    +ress_ne: ∀ Σ : gFunctors, heapG Σ → ∀ (barrierG0 : barrierG Σ) (n : nat), Proper (dist n ==> eq ==> dist n) ress
     barrier_ctx_persistent:                                                                                                                                                                                                                     
       ∀ (Σ : gFunctors) (heapG0 : heapG Σ) (barrierG0 : barrierG Σ) (N : namespace) (γ : gname)                                                                                                                                                 
       (l : loc) (P : iProp Σ), PersistentP (barrier_ctx N γ l P)                                                                                                                                                                                
  • Seems like heapG was added in three places where it was not needed. Why should that have a 1sec impact?

  • Those changes are pretty limited, and these lemmas are mostly internal to the section anyway. Probably Coq's implementation of Proof Using is efficient and gives some minor overhead in very large sections (like in list).

    Don't think we should really care, though. I was mostly concerned that many definitions would get spurious type class parameters, but that is not the case, fortunately.

  • Indeed, nothing that's imported by barrier.proof changes at all.

  • Actually, that statement was entirely wrong. The two versions I compared both had Proof Using everywhere, the only difference is in the Proof Using for barrier.proof

  • All right. Here's the full diff. It's large-ish, i.e., there are actually quite some lemmas that changed their type:

    --- about-old	2017-01-04 13:30:17.753281969 +0100
    +++ about-new	2017-01-04 12:13:11.042545334 +0100
    @@ -12953,7 +12953,7 @@
     cmra_opM_assoc_L: ∀ A : cmraT, LeibnizEquiv A → ∀ (x y : A) (mz : option A), x ⋅ y ⋅? mz = x ⋅ (y ⋅? mz)
     cmra_pcore_r_L: ∀ A : cmraT, LeibnizEquiv A → ∀ x cx : A, pcore x = Some cx → x ⋅ cx = x
     cmra_pcore_dup_L: ∀ A : cmraT, LeibnizEquiv A → ∀ x cx : A, pcore x = Some cx → cx = cx ⋅ cx
    -persistent_dup_L: ∀ (A : cmraT) (x : A), Persistent x → x ≡ x ⋅ x
    +persistent_dup_L: ∀ A : cmraT, LeibnizEquiv A → ∀ x : A, Persistent x → x ≡ x ⋅ x
     cmra_core_r_L: ∀ A : cmraT, LeibnizEquiv A → CMRATotal A → ∀ x : A, x ⋅ core x = x
     cmra_core_l_L: ∀ A : cmraT, LeibnizEquiv A → CMRATotal A → ∀ x : A, core x ⋅ x = x
     cmra_core_idemp_L: ∀ A : cmraT, LeibnizEquiv A → CMRATotal A → ∀ x : A, core (core x) = core x
    @@ -13770,18 +13770,27 @@
     collection_equiv: ∀ A C : Type, ElemOf A C → Equiv C
     collection_subseteq: ∀ A C : Type, ElemOf A C → SubsetEq C
     collection_disjoint: ∀ A C : Type, ElemOf A C → Disjoint C
    -collection_equivalence: ∀ (A C : Type) (H : ElemOf A C), Equivalence equiv
    +collection_equivalence:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → Equivalence equiv
     collections.singleton_proper:
    -  ∀ (A C : Type) (H : ElemOf A C) (H1 : Singleton A C), Proper (eq ==> equiv) singleton
    -elem_of_proper: ∀ (A C : Type) (H : ElemOf A C), Proper (eq ==> equiv ==> iff) elem_of
    -disjoint_proper: ∀ (A C : Type) (H : ElemOf A C), Proper (equiv ==> equiv ==> iff) disjoint
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → Proper (eq ==> equiv) singleton
    +elem_of_proper:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → Proper (eq ==> equiv ==> iff) elem_of
    +disjoint_proper:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → Proper (equiv ==> equiv ==> iff) disjoint
     union_proper:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → Proper (equiv ==> equiv ==> equiv) union
     union_list_proper:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → Proper (equiv ==> equiv) union_list
    -subseteq_proper: ∀ (A C : Type) (H : ElemOf A C), Proper (equiv ==> equiv ==> iff) (subseteq : relation C)
    +subseteq_proper:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → Proper (equiv ==> equiv ==> iff) (subseteq : relation C)
     intersection_proper:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Intersection C)
       (H4 : Difference C), Collection A C → Proper (equiv ==> equiv ==> equiv) intersection
    @@ -13831,7 +13840,9 @@
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C
       → ∀ (x : A) (X Y : C) (P Q : Prop), SetUnfold (x ∈ X) P → SetUnfold (x ∈ Y) Q → SetUnfold (x ∈ X ∪ Y) (P ∨ Q)
    -set_unfold_equiv_same: ∀ (A C : Type) (H : ElemOf A C) (X : C), SetUnfold (X ≡ X) True
    +set_unfold_equiv_same:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → ∀ X : C, SetUnfold (X ≡ X) True
     set_unfold_equiv_empty_l:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C
    @@ -13841,20 +13852,32 @@
       SimpleCollection A C
       → ∀ (P : A → Prop) (X : C), (∀ x : A, SetUnfold (x ∈ X) (P x)) → SetUnfold (X ≡ ∅) (∀ x : A, ¬ P x)
     set_unfold_equiv:
    -  ∀ (A C : Type) (H : ElemOf A C) (P Q : A → Prop) (X Y : C),
    -  (∀ x : A, SetUnfold (x ∈ X) (P x)) → (∀ x : A, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ≡ Y) (∀ x : A, P x ↔ Q x)
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C
    +  → ∀ (P Q : A → Prop) (X Y : C),
    +    (∀ x : A, SetUnfold (x ∈ X) (P x))
    +    → (∀ x : A, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ≡ Y) (∀ x : A, P x ↔ Q x)
     set_unfold_subseteq:
    -  ∀ (A C : Type) (H : ElemOf A C) (P Q : A → Prop) (X Y : C),
    -  (∀ x : A, SetUnfold (x ∈ X) (P x)) → (∀ x : A, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ⊆ Y) (∀ x : A, P x → Q x)
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C
    +  → ∀ (P Q : A → Prop) (X Y : C),
    +    (∀ x : A, SetUnfold (x ∈ X) (P x))
    +    → (∀ x : A, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ⊆ Y) (∀ x : A, P x → Q x)
     set_unfold_subset:
    -  ∀ (A C : Type) (H : ElemOf A C) (P Q : A → Prop) (X Y : C),
    -  (∀ x : A, SetUnfold (x ∈ X) (P x))
    -  → (∀ x : A, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ⊂ Y) ((∀ x : A, P x → Q x) ∧ ¬ (∀ x : A, Q x → P x))
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C
    +  → ∀ (P Q : A → Prop) (X Y : C),
    +    (∀ x : A, SetUnfold (x ∈ X) (P x))
    +    → (∀ x : A, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ⊂ Y) ((∀ x : A, P x → Q x) ∧ ¬ (∀ x : A, Q x → P x))
     set_unfold_disjoint:
    -  ∀ (A C : Type) (H : ElemOf A C) (P Q : A → Prop) (X Y : C),
    -  (∀ x : A, SetUnfold (x ∈ X) (P x))
    -  → (∀ x : A, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ⊥ Y) (∀ x : A, P x → Q x → False)
    -set_unfold_equiv_same_L: ∀ (C : Type) (X : C), SetUnfold (X = X) True
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C
    +  → ∀ (P Q : A → Prop) (X Y : C),
    +    (∀ x : A, SetUnfold (x ∈ X) (P x))
    +    → (∀ x : A, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ⊥ Y) (∀ x : A, P x → Q x → False)
    +set_unfold_equiv_same_L:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → LeibnizEquiv C → ∀ X : C, SetUnfold (X = X) True
     set_unfold_equiv_empty_l_L:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C
    @@ -13866,11 +13889,12 @@
       → LeibnizEquiv C
         → ∀ (P : A → Prop) (X : C), (∀ x : A, SetUnfold (x ∈ X) (P x)) → SetUnfold (X = ∅) (∀ x : A, ¬ P x)
     set_unfold_equiv_L:
    -  ∀ (A C : Type) (H : ElemOf A C),
    -  LeibnizEquiv C
    -  → ∀ (P Q : A → Prop) (X Y : C),
    -    (∀ x : A, SetUnfold (x ∈ X) (P x))
    -    → (∀ x : A, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X = Y) (∀ x : A, P x ↔ Q x)
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C
    +  → LeibnizEquiv C
    +    → ∀ (P Q : A → Prop) (X Y : C),
    +      (∀ x : A, SetUnfold (x ∈ X) (P x))
    +      → (∀ x : A, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X = Y) (∀ x : A, P x ↔ Q x)
     set_unfold_intersection:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Intersection C)
       (H4 : Difference C),
    @@ -13917,7 +13941,9 @@
     set_unfold_included:
       ∀ (A : Type) (l k : list A) (P Q : A → Prop),
       (∀ x : A, SetUnfold (x ∈ l) (P x)) → (∀ x : A, SetUnfold (x ∈ k) (Q x)) → SetUnfold (l ⊆ k) (∀ x : A, P x → Q x)
    -elem_of_equiv: ∀ (A C : Type) (H : ElemOf A C) (X Y : C), X ≡ Y ↔ (∀ x : A, x ∈ X ↔ x ∈ Y)
    +elem_of_equiv:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → ∀ X Y : C, X ≡ Y ↔ (∀ x : A, x ∈ X ↔ x ∈ Y)
     collection_equiv_spec:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ X Y : C, X ≡ Y ↔ X ⊆ Y ⊆ X
    @@ -13945,9 +13971,12 @@
     union_least:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ X Y Z : C, X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z
    -elem_of_subseteq: ∀ (A C : Type) (H : ElemOf A C) (X Y : C), X ⊆ Y ↔ (∀ x : A, x ∈ X → x ∈ Y)
    +elem_of_subseteq:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → ∀ X Y : C, X ⊆ Y ↔ (∀ x : A, x ∈ X → x ∈ Y)
     elem_of_subset:
    -  ∀ (A C : Type) (H : ElemOf A C) (X Y : C), X ⊂ Y ↔ (∀ x : A, x ∈ X → x ∈ Y) ∧ ¬ (∀ x : A, x ∈ Y → x ∈ X)
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → ∀ X Y : C, X ⊂ Y ↔ (∀ x : A, x ∈ X → x ∈ Y) ∧ ¬ (∀ x : A, x ∈ Y → x ∈ X)
     not_elem_of_union:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ (x : A) (X Y : C), x ∉ X ∪ Y ↔ (x ∉ X) ∧ x ∉ Y
    @@ -14023,7 +14052,9 @@
     not_elem_of_singleton:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ x y : A, x ∉ {[y]} ↔ x ≠ y
    -elem_of_disjoint: ∀ (A C : Type) (H : ElemOf A C) (X Y : C), X ⊥ Y ↔ (∀ x : A, x ∈ X → x ∈ Y → False)
    +elem_of_disjoint:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → ∀ X Y : C, X ⊥ Y ↔ (∀ x : A, x ∈ X → x ∈ Y → False)
     disjoint_sym:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → Symmetric disjoint
    @@ -14048,8 +14079,12 @@
     elem_of_union_list:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ (Xs : list C) (x : A), x ∈ ⋃ Xs ↔ (∃ X : C, X ∈ Xs ∧ x ∈ X)
    -union_list_nil: ∀ (C : Type) (H0 : Empty C) (H2 : Union C), ⋃ [] = ∅
    -union_list_cons: ∀ (C : Type) (H0 : Empty C) (H2 : Union C) (X : C) (Xs : list C), ⋃ (X :: Xs) = X ∪ ⋃ Xs
    +union_list_nil:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → ⋃ [] = ∅
    +union_list_cons:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → ∀ (X : C) (Xs : list C), ⋃ (X :: Xs) = X ∪ ⋃ Xs
     union_list_singleton:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ X : C, ⋃ [X] ≡ X
    @@ -14065,7 +14100,9 @@
     empty_union_list:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ Xs : list C, ⋃ Xs ≡ ∅ ↔ Forall (λ Y : C, Y ≡ ∅) Xs
    -elem_of_equiv_L: ∀ (A C : Type) (H : ElemOf A C), LeibnizEquiv C → ∀ X Y : C, X = Y ↔ (∀ x : A, x ∈ X ↔ x ∈ Y)
    +elem_of_equiv_L:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → LeibnizEquiv C → ∀ X Y : C, X = Y ↔ (∀ x : A, x ∈ X ↔ x ∈ Y)
     collection_equiv_spec_L:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → LeibnizEquiv C → ∀ X Y : C, X = Y ↔ X ⊆ Y ⊆ X
    @@ -14276,10 +14313,10 @@
       (H4 : Difference C), Collection A C → LeibnizEquiv C → ∀ X Y Z : C, X ∩ Y ∪ Z = (X ∪ Z) ∩ (Y ∪ Z)
     intersection_union_l_L:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Intersection C)
    -  (H4 : Difference C), Collection A C → ∀ X Y Z : C, X ∩ (Y ∪ Z) ≡ X ∩ Y ∪ X ∩ Z
    +  (H4 : Difference C), Collection A C → LeibnizEquiv C → ∀ X Y Z : C, X ∩ (Y ∪ Z) ≡ X ∩ Y ∪ X ∩ Z
     intersection_union_r_L:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Intersection C)
    -  (H4 : Difference C), Collection A C → ∀ X Y Z : C, (X ∪ Y) ∩ Z ≡ X ∩ Z ∪ Y ∩ Z
    +  (H4 : Difference C), Collection A C → LeibnizEquiv C → ∀ X Y Z : C, (X ∪ Y) ∩ Z ≡ X ∩ Z ∪ Y ∩ Z
     difference_twice_L:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Intersection C)
       (H4 : Difference C), Collection A C → LeibnizEquiv C → ∀ X Y : C, X ∖ Y ∖ Y = X ∖ Y
    @@ -14362,10 +14399,12 @@
     set_unfold_of_list:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ (l : list A) (x : A) (P : Prop), SetUnfold (x ∈ l) P → SetUnfold (x ∈ of_list l) P
    -of_list_nil: ∀ (A C : Type) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C), of_list [] = ∅
    +of_list_nil:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → of_list [] = ∅
     of_list_cons:
    -  ∀ (A C : Type) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (x : A) (l : list A),
    -  of_list (x :: l) = {[x]} ∪ of_list l
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → ∀ (x : A) (l : list A), of_list (x :: l) = {[x]} ∪ of_list l
     of_list_app:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ l1 l2 : list A, of_list (l1 ++ l2) ≡ of_list l1 ∪ of_list l2
    @@ -14441,11 +14480,11 @@
       ∀ (A B : Type) (H : ElemOf A B) (H0 : Empty B) (H1 : Singleton A B) (H2 : Union B),
       SimpleCollection A B → ∀ (P : A → Prop) (X Y : B), set_Exists P (X ∪ Y) → set_Exists P X ∨ set_Exists P Y
     set_Forall_weaken:
    -  ∀ (A B : Type) (H : ElemOf A B) (P Q : A → Prop),
    -  (∀ x : A, P x → Q x) → ∀ X : B, set_Forall P X → set_Forall Q X
    +  ∀ (A B : Type) (H : ElemOf A B) (H0 : Empty B) (H1 : Singleton A B) (H2 : Union B),
    +  SimpleCollection A B → ∀ P Q : A → Prop, (∀ x : A, P x → Q x) → ∀ X : B, set_Forall P X → set_Forall Q X
     set_Exists_weaken:
    -  ∀ (A B : Type) (H : ElemOf A B) (P Q : A → Prop),
    -  (∀ x : A, P x → Q x) → ∀ X : B, set_Exists P X → set_Exists Q X
    +  ∀ (A B : Type) (H : ElemOf A B) (H0 : Empty B) (H1 : Singleton A B) (H2 : Union B),
    +  SimpleCollection A B → ∀ P Q : A → Prop, (∀ x : A, P x → Q x) → ∀ X : B, set_Exists P X → set_Exists Q X
     fresh_list: ∀ A C : Type, Fresh A C → Union C → Singleton A C → nat → C → list A
     Forall_fresh: ∀ A C : Type, ElemOf A C → C → list A → Prop
     Forall_fresh_nil: ∀ (A C : Type) (H : ElemOf A C) (X : C), Forall_fresh X []
    @@ -14466,17 +14505,21 @@
     exist_fresh:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Fresh A C),
       FreshSpec A C → ∀ X : C, ∃ x : A, x ∉ X
    -Forall_fresh_NoDup: ∀ (A C : Type) (H : ElemOf A C) (X : C) (xs : list A), Forall_fresh X xs → NoDup xs
    +Forall_fresh_NoDup:
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Fresh A C),
    +  FreshSpec A C → ∀ (X : C) (xs : list A), Forall_fresh X xs → NoDup xs
     Forall_fresh_elem_of:
    -  ∀ (A C : Type) (H : ElemOf A C) (X : C) (xs : list A) (x : A), Forall_fresh X xs → x ∈ xs → x ∉ X
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Fresh A C),
    +  FreshSpec A C → ∀ (X : C) (xs : list A) (x : A), Forall_fresh X xs → x ∈ xs → x ∉ X
     Forall_fresh_alt:
    -  ∀ (A C : Type) (H : ElemOf A C) (X : C) (xs : list A), Forall_fresh X xs ↔ NoDup xs ∧ (∀ x : A, x ∈ xs → x ∉ X)
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Fresh A C),
    +  FreshSpec A C → ∀ (X : C) (xs : list A), Forall_fresh X xs ↔ NoDup xs ∧ (∀ x : A, x ∈ xs → x ∉ X)
     Forall_fresh_subseteq:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Fresh A C),
       FreshSpec A C → ∀ (X Y : C) (xs : list A), Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs
     fresh_list_length:
    -  ∀ (A C : Type) (H1 : Singleton A C) (H2 : Union C) (H3 : Fresh A C) (n : nat) (X : C),
    -  length (fresh_list n X) = n
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Fresh A C),
    +  FreshSpec A C → ∀ (n : nat) (X : C), length (fresh_list n X) = n
     fresh_list_is_fresh:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Fresh A C),
       FreshSpec A C → ∀ (n : nat) (X : C) (x : A), x ∈ fresh_list n X → x ∉ X
    @@ -14568,7 +14611,9 @@
     set_finite_subseteq:
       ∀ (A B : Type) (H : ElemOf A B) (H0 : Empty B) (H1 : Singleton A B) (H2 : Union B),
       SimpleCollection A B → Proper (subseteq --> impl) set_finite
    -set_finite_proper: ∀ (A B : Type) (H : ElemOf A B), Proper (equiv ==> iff) set_finite
    +set_finite_proper:
    +  ∀ (A B : Type) (H : ElemOf A B) (H0 : Empty B) (H1 : Singleton A B) (H2 : Union B),
    +  SimpleCollection A B → Proper (equiv ==> iff) set_finite
     empty_finite:
       ∀ (A B : Type) (H : ElemOf A B) (H0 : Empty B) (H1 : Singleton A B) (H2 : Union B),
       SimpleCollection A B → set_finite ∅
    @@ -14617,17 +14662,20 @@
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ (R : relation A) (x : A), Proper (equiv ==> iff) (minimal R x)
     minimal_anti_symm_1:
    -  ∀ (A C : Type) (H : ElemOf A C) (R : relation A),
    -  AntiSymm eq R → ∀ (X : C) (x y : A), minimal R x X → y ∈ X → R y x → x = y
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C
    +  → ∀ R : relation A, AntiSymm eq R → ∀ (X : C) (x y : A), minimal R x X → y ∈ X → R y x → x = y
     minimal_anti_symm:
    -  ∀ (A C : Type) (H : ElemOf A C) (R : relation A),
    -  AntiSymm eq R → ∀ (X : C) (x : A), minimal R x X ↔ (∀ y : A, y ∈ X → R y x → x = y)
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C
    +  → ∀ R : relation A, AntiSymm eq R → ∀ (X : C) (x : A), minimal R x X ↔ (∀ y : A, y ∈ X → R y x → x = y)
     minimal_strict_1:
    -  ∀ (A C : Type) (H : ElemOf A C) (R : relation A),
    -  StrictOrder R → ∀ (X : C) (x y : A), minimal R x X → y ∈ X → ¬ R y x
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C → ∀ R : relation A, StrictOrder R → ∀ (X : C) (x y : A), minimal R x X → y ∈ X → ¬ R y x
     minimal_strict:
    -  ∀ (A C : Type) (H : ElemOf A C) (R : relation A),
    -  StrictOrder R → ∀ (X : C) (x : A), minimal R x X ↔ (∀ y : A, y ∈ X → ¬ R y x)
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C
    +  → ∀ R : relation A, StrictOrder R → ∀ (X : C) (x : A), minimal R x X ↔ (∀ y : A, y ∈ X → ¬ R y x)
     empty_minimal:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ (R : relation A) (x : A), minimal R x ∅
    @@ -14644,8 +14692,9 @@
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
       SimpleCollection A C → ∀ (R : relation A) (X Y : C) (x : A), minimal R x X → Y ⊆ X → minimal R x Y
     minimal_weaken:
    -  ∀ (A C : Type) (H : ElemOf A C) (R : relation A),
    -  Transitive R → ∀ (X : C) (x x' : A), minimal R x X → R x' x → minimal R x' X
    +  ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C),
    +  SimpleCollection A C
    +  → ∀ R : relation A, Transitive R → ∀ (X : C) (x x' : A), minimal R x X → R x' x → minimal R x' X
     coq_tactics.envs: ucmraT → Type
     coq_tactics.Envs: ∀ M : ucmraT, environments.env (uPred M) → environments.env (uPred M) → coq_tactics.envs M
     coq_tactics.env_persistent: ∀ M : ucmraT, coq_tactics.envs M → environments.env (uPred M)
    @@ -15111,7 +15160,7 @@
         → ∀ p p0 : positive, choose_step P p p0 → P0 p p0
     choose_step_acc:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : Countable A) (P : A → Prop),
    -  (∃ x : A, P x) → Acc (choose_step P) 1%positive
    +  (∀ x : A, Decision (P x)) → (∃ x : A, P x) → Acc (choose_step P) 1%positive
     choose_go:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : Countable A) (P : A → Prop),
       (∀ x : A, Decision (P x)) → ∀ i : positive, Acc (choose_step P) i → A
    @@ -15674,21 +15723,25 @@
       LanguageCtx (ectx_lang expr) (ectx_language.fill K)
     ectx_lifting.wp_ectx_bind:
       ∀ (expr val ectx state : Type) (Λ : EctxLanguage expr val ectx state) (Σ : gFunctors)
    -  (irisG0 : irisG (ectx_lang expr) Σ) (E : coPset) (e : expr) (K : ectx) (Φ : val → iProp Σ),
    -  WP e @ E {{ v, WP ectx_language.fill K (language.of_val v) @ E {{ v, Φ v }} }} -∗
    -  WP ectx_language.fill K e @ E {{ v, Φ v }}
    +  (irisG0 : irisG (ectx_lang expr) Σ),
    +  Inhabited state
    +  → ∀ (E : coPset) (e : expr) (K : ectx) (Φ : val → iProp Σ),
    +    WP e @ E {{ v, WP ectx_language.fill K (language.of_val v) @ E {{ v, Φ v }} }} -∗
    +    WP ectx_language.fill K e @ E {{ v, Φ v }}
     ectx_lifting.wp_lift_head_step:
       ∀ (expr val ectx state : Type) (Λ : EctxLanguage expr val ectx state) (Σ : gFunctors)
    -  (irisG0 : irisG (ectx_lang expr) Σ) (E : coPset) (Φ : val → iProp Σ) (e1 : expr),
    -  language.to_val e1 = None
    -  → (∀ σ1 : language.state (ectx_lang expr),
    -     state_interp σ1 ={E,∅}=∗ ⌜head_reducible e1 σ1⌝
    -                              ∗ ▷ (∀ (e2 : expr) (σ2 : language.state (ectx_lang expr)) 
    -                                   (efs : list expr),
    -                                   ⌜ectx_language.head_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗ 
    -                                   state_interp σ2
    -                                   ∗ WP e2 @ E {{ v, Φ v }} ∗ ([∗ list] ef ∈ efs, WP ef {{ _, True }}))) -∗
    -    WP e1 @ E {{ v, Φ v }}
    +  (irisG0 : irisG (ectx_lang expr) Σ),
    +  Inhabited state
    +  → ∀ (E : coPset) (Φ : val → iProp Σ) (e1 : expr),
    +    language.to_val e1 = None
    +    → (∀ σ1 : language.state (ectx_lang expr),
    +       state_interp σ1 ={E,∅}=∗ ⌜head_reducible e1 σ1⌝
    +                                ∗ ▷ (∀ (e2 : expr) (σ2 : language.state (ectx_lang expr)) 
    +                                     (efs : list expr),
    +                                     ⌜ectx_language.head_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗ 
    +                                     state_interp σ2
    +                                     ∗ WP e2 @ E {{ v, Φ v }} ∗ ([∗ list] ef ∈ efs, WP ef {{ _, True }}))) -∗
    +      WP e1 @ E {{ v, Φ v }}
     ectx_lifting.wp_lift_pure_head_step:
       ∀ (expr val ectx state : Type) (Λ : EctxLanguage expr val ectx state) (Σ : gFunctors)
       (irisG0 : irisG (ectx_lang expr) Σ),
    @@ -15703,35 +15756,41 @@
             Φ v }}
     ectx_lifting.wp_lift_atomic_head_step:
       ∀ (expr val ectx state : Type) (Λ : EctxLanguage expr val ectx state) (Σ : gFunctors)
    -  (irisG0 : irisG (ectx_lang expr) Σ) (E : coPset) (Φ : val → iProp Σ) (e1 : expr),
    -  language.to_val e1 = None
    -  → (∀ σ1 : language.state (ectx_lang expr),
    -     state_interp σ1 ={E}=∗ ⌜head_reducible e1 σ1⌝
    -                            ∗ ▷ (∀ (e2 : expr) (σ2 : language.state (ectx_lang expr)) 
    -                                 (efs : list expr),
    -                                 ⌜ectx_language.head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗ state_interp σ2
    -                                                                                  ∗ from_option Φ 
    +  (irisG0 : irisG (ectx_lang expr) Σ),
    +  Inhabited state
    +  → ∀ (E : coPset) (Φ : val → iProp Σ) (e1 : expr),
    +    language.to_val e1 = None
    +    → (∀ σ1 : language.state (ectx_lang expr),
    +       state_interp σ1 ={E}=∗ ⌜head_reducible e1 σ1⌝
    +                              ∗ ▷ (∀ (e2 : expr) (σ2 : language.state (ectx_lang expr)) 
    +                                   (efs : list expr),
    +                                   ⌜ectx_language.head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗ state_interp σ2
    +                                                                                    ∗ 
    +                                                                                    from_option Φ 
                                                                                          False 
                                                                                          (language.to_val e2)
    
                                                                                         ([∗ list] ef ∈ efs, WP ef {{ _, 
                                                                                          True }}))) -∗
    -    WP e1 @ E {{ v, Φ v }}
    +      WP e1 @ E {{ v, Φ v }}
     ectx_lifting.wp_lift_atomic_head_step_no_fork:
       ∀ (expr val ectx state : Type) (Λ : EctxLanguage expr val ectx state) (Σ : gFunctors)
    -  (irisG0 : irisG (ectx_lang expr) Σ) (E : coPset) (Φ : val → iProp Σ) (e1 : expr),
    -  language.to_val e1 = None
    -  → (∀ σ1 : language.state (ectx_lang expr),
    -     state_interp σ1 ={E}=∗ ⌜head_reducible e1 σ1⌝
    -                            ∗ ▷ (∀ (e2 : expr) (σ2 : language.state (ectx_lang expr)) 
    -                                 (efs : list expr),
    -                                 ⌜ectx_language.head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗ ⌜efs = []⌝
    -                                                                                  ∗ state_interp σ2
    +  (irisG0 : irisG (ectx_lang expr) Σ),
    +  Inhabited state
    +  → ∀ (E : coPset) (Φ : val → iProp Σ) (e1 : expr),
    +    language.to_val e1 = None
    +    → (∀ σ1 : language.state (ectx_lang expr),
    +       state_interp σ1 ={E}=∗ ⌜head_reducible e1 σ1⌝
    +                              ∗ ▷ (∀ (e2 : expr) (σ2 : language.state (ectx_lang expr)) 
    +                                   (efs : list expr),
    +                                   ⌜ectx_language.head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗ ⌜efs = []⌝
    +                                                                                    ∗ 
    +                                                                                    state_interp σ2
    
                                                                                         from_option Φ 
                                                                                          False 
                                                                                          (language.to_val e2))) -∗
    -    WP e1 @ E {{ v, Φ v }}
    +      WP e1 @ E {{ v, Φ v }}
     ectx_lifting.wp_lift_pure_det_head_step:
       ∀ (expr val ectx state : Type) (Λ : EctxLanguage expr val ectx state) (Σ : gFunctors)
       (irisG0 : irisG (ectx_lang expr) Σ),
    @@ -16914,21 +16973,31 @@
       → (∀ A : Type, Empty (M A))
         → (∀ A : Type, FinMapToList K A (M A)) → ∀ A B : Type, (K → A → option B) → M A → M B
     map_equivalence:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (H7 : Equiv A),
    -  Equivalence (equiv : relation A) → Equivalence (equiv : relation (M A))
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M
    +  → ∀ (A : Type) (H7 : Equiv A), Equivalence (equiv : relation A) → Equivalence (equiv : relation (M A))
     lookup_proper:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (H7 : Equiv A) 
    -  (i : K), Proper (equiv ==> equiv) (lookup i)
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M
    +  → ∀ (A : Type) (H7 : Equiv A), Equivalence (equiv : relation A) → ∀ i : K, Proper (equiv ==> equiv) (lookup i)
     partial_alter_proper:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
       (EqDecision0 : EqDecision K),
    -  FinMap K M → ∀ (A : Type) (H7 : Equiv A), Proper ((equiv ==> equiv) ==> eq ==> equiv ==> equiv) partial_alter
    +  FinMap K M
    +  → ∀ (A : Type) (H7 : Equiv A),
    +    Equivalence (equiv : relation A) → Proper ((equiv ==> equiv) ==> eq ==> equiv ==> equiv) partial_alter
     insert_proper:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
       (EqDecision0 : EqDecision K),
    -  FinMap K M → ∀ (A : Type) (H7 : Equiv A) (i : K), Proper (equiv ==> equiv ==> equiv) (insert i)
    +  FinMap K M
    +  → ∀ (A : Type) (H7 : Equiv A),
    +    Equivalence (equiv : relation A) → ∀ i : K, Proper (equiv ==> equiv ==> equiv) (insert i)
     singleton_proper:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    @@ -16940,27 +17009,34 @@
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
       (EqDecision0 : EqDecision K),
    -  FinMap K M → ∀ (A : Type) (H7 : Equiv A) (i : K), Proper (equiv ==> equiv) (delete i)
    +  FinMap K M
    +  → ∀ (A : Type) (H7 : Equiv A), Equivalence (equiv : relation A) → ∀ i : K, Proper (equiv ==> equiv) (delete i)
     alter_proper:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
       (EqDecision0 : EqDecision K),
    -  FinMap K M → ∀ (A : Type) (H7 : Equiv A), Proper ((equiv ==> equiv) ==> eq ==> equiv ==> equiv) alter
    +  FinMap K M
    +  → ∀ (A : Type) (H7 : Equiv A),
    +    Equivalence (equiv : relation A) → Proper ((equiv ==> equiv) ==> eq ==> equiv ==> equiv) alter
     merge_ext:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
       (EqDecision0 : EqDecision K),
       FinMap K M
    -  → ∀ (A : Type) (H7 : Equiv A) (f g : option A → option A → option A),
    -    DiagNone f
    -    → DiagNone g
    -      → (equiv ==> equiv ==> equiv)%signature f g → (equiv ==> equiv ==> equiv)%signature (merge f) (merge g)
    +  → ∀ (A : Type) (H7 : Equiv A),
    +    Equivalence (equiv : relation A)
    +    → ∀ f g : option A → option A → option A,
    +      DiagNone f
    +      → DiagNone g
    +        → (equiv ==> equiv ==> equiv)%signature f g → (equiv ==> equiv ==> equiv)%signature (merge f) (merge g)
     union_with_proper:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
       (EqDecision0 : EqDecision K),
       FinMap K M
    -  → ∀ (A : Type) (H7 : Equiv A), Proper ((equiv ==> equiv ==> equiv) ==> equiv ==> equiv ==> equiv) union_with
    +  → ∀ (A : Type) (H7 : Equiv A),
    +    Equivalence (equiv : relation A)
    +    → Proper ((equiv ==> equiv ==> equiv) ==> equiv ==> equiv ==> equiv) union_with
     map_leibniz:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    @@ -16972,44 +17048,62 @@
       (EqDecision0 : EqDecision K),
       FinMap K M → ∀ (A : Type) (H7 : Equiv A), Equivalence (equiv : relation A) → ∀ m : M A, m ≡ ∅ ↔ m = ∅
     map_equiv_lookup_l:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (H7 : Equiv A) 
    -  (m1 m2 : M A) (i : K) (x : A), m1 ≡ m2 → m1 !! i = Some x → ∃ y : A, m2 !! i = Some y ∧ x ≡ y
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M
    +  → ∀ (A : Type) (H7 : Equiv A),
    +    Equivalence (equiv : relation A)
    +    → ∀ (m1 m2 : M A) (i : K) (x : A), m1 ≡ m2 → m1 !! i = Some x → ∃ y : A, m2 !! i = Some y ∧ x ≡ y
     map_fmap_proper:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
       (EqDecision0 : EqDecision K),
       FinMap K M
    -  → ∀ (A : Type) (H7 : Equiv A) (B : Type) (H8 : Equiv B) (f : A → B),
    -    Proper (equiv ==> equiv) f → Proper (equiv ==> equiv) (fmap f)
    +  → ∀ (A : Type) (H7 : Equiv A),
    +    Equivalence (equiv : relation A)
    +    → ∀ (B : Type) (H8 : Equiv B) (f : A → B), Proper (equiv ==> equiv) f → Proper (equiv ==> equiv) (fmap f)
     map_eq_iff:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
       (EqDecision0 : EqDecision K), FinMap K M → ∀ (A : Type) (m1 m2 : M A), m1 = m2 ↔ (∀ i : K, m1 !! i = m2 !! i)
     map_subseteq_spec:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m2 : M A),
    -  m1 ⊆ m2 ↔ (∀ (i : K) (x : A), m1 !! i = Some x → m2 !! i = Some x)
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M → ∀ (A : Type) (m1 m2 : M A), m1 ⊆ m2 ↔ (∀ (i : K) (x : A), m1 !! i = Some x → m2 !! i = Some x)
     PreOrder_instance_0:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (R : relation A),
    -  PreOrder R → PreOrder (map_included R)
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K), FinMap K M → ∀ (A : Type) (R : relation A), PreOrder R → PreOrder (map_included R)
     PartialOrder_instance_0:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
       (EqDecision0 : EqDecision K), FinMap K M → ∀ A : Type, PartialOrder (subseteq : relation (M A))
     lookup_weaken:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m2 : M A) 
    -  (i : K) (x : A), m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M → ∀ (A : Type) (m1 m2 : M A) (i : K) (x : A), m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x
     lookup_weaken_is_Some:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m2 : M A) 
    -  (i : K), is_Some (m1 !! i) → m1 ⊆ m2 → is_Some (m2 !! i)
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M → ∀ (A : Type) (m1 m2 : M A) (i : K), is_Some (m1 !! i) → m1 ⊆ m2 → is_Some (m2 !! i)
     lookup_weaken_None:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m2 : M A) 
    -  (i : K), m2 !! i = None → m1 ⊆ m2 → m1 !! i = None
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M → ∀ (A : Type) (m1 m2 : M A) (i : K), m2 !! i = None → m1 ⊆ m2 → m1 !! i = None
     lookup_weaken_inv:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m2 : M A) 
    -  (i : K) (x y : A), m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some y → x = y
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M → ∀ (A : Type) (m1 m2 : M A) (i : K) (x y : A), m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some y → x = y
     lookup_ne:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m : M A) 
    -  (i j : K), m !! i ≠ m !! j → i ≠ j
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K), FinMap K M → ∀ (A : Type) (m : M A) (i j : K), m !! i ≠ m !! j → i ≠ j
     map_empty:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    @@ -17289,8 +17383,9 @@
       → ∀ (A : Type) (m1 m2 : M A) (i : K) (x : A),
         m1 !! i = None → <[i:=x]> m1 ⊂ m2 → ∃ m2' : M A, m2 = <[i:=x]> m2' ∧ m1 ⊂ m2' ∧ m2' !! i = None
     insert_empty:
    -  ∀ (K : Type) (M : Type → Type) (H1 : ∀ A : Type, Empty (M A)) (H2 : ∀ A : Type, PartialAlter K A (M A))
    -  (A : Type) (i : K) (x : A), <[i:=x]> ∅ = {[i := x]}
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K), FinMap K M → ∀ (A : Type) (i : K) (x : A), <[i:=x]> ∅ = {[i := x]}
     insert_non_empty:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    @@ -17482,11 +17577,15 @@
       (EqDecision0 : EqDecision K),
       FinMap K M → ∀ (A : Type) (m1 : M A) (l2 : list (K * A)), map_to_list m1 ≡ₚ l2 → m1 = map_of_list l2
     map_of_list_nil:
    -  ∀ (K : Type) (M : Type → Type) (H1 : ∀ A : Type, Empty (M A)) (H2 : ∀ A : Type, PartialAlter K A (M A))
    -  (A : Type), map_of_list [] = ∅
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K), FinMap K M → ∀ A : Type, map_of_list [] = ∅
     map_of_list_cons:
    -  ∀ (K : Type) (M : Type → Type) (H1 : ∀ A : Type, Empty (M A)) (H2 : ∀ A : Type, PartialAlter K A (M A))
    -  (A : Type) (l : list (K * A)) (i : K) (x : A), map_of_list ((i, x) :: l) = <[i:=x]> (map_of_list l)
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M
    +  → ∀ (A : Type) (l : list (K * A)) (i : K) (x : A), map_of_list ((i, x) :: l) = <[i:=x]> (map_of_list l)
     map_of_list_fmap:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    @@ -17584,8 +17683,12 @@
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
       (EqDecision0 : EqDecision K), FinMap K M → ∀ (A : Type) (P : K → A → Prop), map_Forall P ∅
     map_Forall_impl:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (P Q : K → A → Prop) 
    -  (m : M A), map_Forall P m → (∀ (i : K) (x : A), P i x → Q i x) → map_Forall Q m
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M
    +  → ∀ (A : Type) (P Q : K → A → Prop) (m : M A),
    +    map_Forall P m → (∀ (i : K) (x : A), P i x → Q i x) → map_Forall Q m
     map_Forall_insert_11:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    @@ -17814,11 +17917,16 @@
                  ∨ (∃ x : A, m1 !! i = Some x ∧ m2 !! i = None ∧ ¬ P x)
                    ∨ (∃ y : B, m1 !! i = None ∧ m2 !! i = Some y ∧ ¬ Q y))
     map_disjoint_spec:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m2 : M A),
    -  m1 ⊥ₘ m2 ↔ (∀ (i : K) (x y : A), m1 !! i = Some x → m2 !! i = Some y → False)
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M
    +  → ∀ (A : Type) (m1 m2 : M A), m1 ⊥ₘ m2 ↔ (∀ (i : K) (x y : A), m1 !! i = Some x → m2 !! i = Some y → False)
     map_disjoint_alt:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m2 : M A),
    -  m1 ⊥ₘ m2 ↔ (∀ i : K, m1 !! i = None ∨ m2 !! i = None)
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M → ∀ (A : Type) (m1 m2 : M A), m1 ⊥ₘ m2 ↔ (∀ i : K, m1 !! i = None ∨ m2 !! i = None)
     map_not_disjoint:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    @@ -17826,8 +17934,9 @@
       FinMap K M
       → ∀ (A : Type) (m1 m2 : M A), ¬ m1 ⊥ₘ m2 ↔ (∃ (i : K) (x1 x2 : A), m1 !! i = Some x1 ∧ m2 !! i = Some x2)
     map_disjoint_sym:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type),
    -  Symmetric (map_disjoint : relation (M A))
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K), FinMap K M → ∀ A : Type, Symmetric (map_disjoint : relation (M A))
     map_disjoint_empty_l:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    @@ -17837,20 +17946,28 @@
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
       (EqDecision0 : EqDecision K), FinMap K M → ∀ (A : Type) (m : M A), m ⊥ₘ ∅
     map_disjoint_weaken:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m1' m2 m2' : M A),
    -  m1' ⊥ₘ m2' → m1 ⊆ m1' → m2 ⊆ m2' → m1 ⊥ₘ m2
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M → ∀ (A : Type) (m1 m1' m2 m2' : M A), m1' ⊥ₘ m2' → m1 ⊆ m1' → m2 ⊆ m2' → m1 ⊥ₘ m2
     map_disjoint_weaken_l:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m1' m2 : M A),
    -  m1' ⊥ₘ m2 → m1 ⊆ m1' → m1 ⊥ₘ m2
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K), FinMap K M → ∀ (A : Type) (m1 m1' m2 : M A), m1' ⊥ₘ m2 → m1 ⊆ m1' → m1 ⊥ₘ m2
     map_disjoint_weaken_r:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m2 m2' : M A),
    -  m1 ⊥ₘ m2' → m2 ⊆ m2' → m1 ⊥ₘ m2
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K), FinMap K M → ∀ (A : Type) (m1 m2 m2' : M A), m1 ⊥ₘ m2' → m2 ⊆ m2' → m1 ⊥ₘ m2
     map_disjoint_Some_l:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m2 : M A) 
    -  (i : K) (x : A), m1 ⊥ₘ m2 → m1 !! i = Some x → m2 !! i = None
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M → ∀ (A : Type) (m1 m2 : M A) (i : K) (x : A), m1 ⊥ₘ m2 → m1 !! i = Some x → m2 !! i = None
     map_disjoint_Some_r:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (m1 m2 : M A) 
    -  (i : K) (x : A), m1 ⊥ₘ m2 → m2 !! i = Some x → m1 !! i = None
    +  ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
    +  (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    +  (EqDecision0 : EqDecision K),
    +  FinMap K M → ∀ (A : Type) (m1 m2 : M A) (i : K) (x : A), m1 ⊥ₘ m2 → m2 !! i = Some x → m1 !! i = None
     map_disjoint_singleton_l:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    @@ -18396,10 +18513,10 @@
       (H0 : finite.Finite B) (f : A → B), Inj eq eq f → Surj eq f → finite.card A = finite.card B
     finite.Forall_finite:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (P : A → Prop),
    -  Forall P (finite.enum A) ↔ (∀ x : A, P x)
    +  (∀ x : A, Decision (P x)) → Forall P (finite.enum A) ↔ (∀ x : A, P x)
     finite.Exists_finite:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (P : A → Prop),
    -  Exists P (finite.enum A) ↔ (∃ x : A, P x)
    +  (∀ x : A, Decision (P x)) → Exists P (finite.enum A) ↔ (∃ x : A, P x)
     finite.forall_dec:
       ∀ (A : Type) (EqDecision0 : EqDecision A),
       finite.Finite A → ∀ P : A → Prop, (∀ x : A, Decision (P x)) → Decision (∀ x : A, P x)
    @@ -18894,15 +19011,19 @@
       FreshSpec K (gset K)
       → ∀ (m : gmap K A) (x : A), ✓ x → m ~~>: (λ m' : gmap K A, ∃ i : K, m' = <[i:=x]> m ∧ m !! i = None)
     gmap.alloc_unit_singleton_updateP:
    -  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (P : A → Prop) 
    -  (Q : gmap K A → Prop) (u : A) (i : K),
    -  ✓ u → LeftId equiv u op → u ~~>: P → (∀ y : A, P y → Q {[i := y]}) → ∅ ~~>: Q
    +  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (H0 : Fresh K (gset K)),
    +  FreshSpec K (gset K)
    +  → ∀ (P : A → Prop) (Q : gmap K A → Prop) (u : A) (i : K),
    +    ✓ u → LeftId equiv u op → u ~~>: P → (∀ y : A, P y → Q {[i := y]}) → ∅ ~~>: Q
     gmap.alloc_unit_singleton_updateP':
    -  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (P : A → Prop) 
    -  (u : A) (i : K), ✓ u → LeftId equiv u op → u ~~>: P → ∅ ~~>: (λ m : gmap K A, ∃ y : A, m = {[i := y]} ∧ P y)
    +  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (H0 : Fresh K (gset K)),
    +  FreshSpec K (gset K)
    +  → ∀ (P : A → Prop) (u : A) (i : K),
    +    ✓ u → LeftId equiv u op → u ~~>: P → ∅ ~~>: (λ m : gmap K A, ∃ y : A, m = {[i := y]} ∧ P y)
     gmap.alloc_unit_singleton_update:
    -  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (u : A) (i : K) 
    -  (y : A), ✓ u → LeftId equiv u op → u ~~> y → (∅ : gmap K A) ~~> {[i := y]}
    +  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (H0 : Fresh K (gset K)),
    +  FreshSpec K (gset K)
    +  → ∀ (u : A) (i : K) (y : A), ✓ u → LeftId equiv u op → u ~~> y → (∅ : gmap K A) ~~> {[i := y]}
     gmap.alloc_local_update:
       ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (m1 m2 : gmap K A) 
       (i : K) (x : A), m1 !! i = None → ✓ x → local_updates.local_update (m1, m2) (<[i:=x]> m1, <[i:=x]> m2)
    @@ -19475,17 +19596,17 @@
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
       (∀ a : A, Cofe (B a)) → Cofe (iprod.iprodC B)
     iprod.iprod_insert_ne:
    -  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT) (n : nat) 
    -  (x : A), Proper (dist n ==> dist n ==> dist n) (iprod.iprod_insert x)
    +  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
    +  EqDecision A → ∀ (n : nat) (x : A), Proper (dist n ==> dist n ==> dist n) (iprod.iprod_insert x)
     iprod.iprod_insert_proper:
    -  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT) (x : A),
    -  Proper (equiv ==> equiv ==> equiv) (iprod.iprod_insert x)
    +  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
    +  EqDecision A → ∀ x : A, Proper (equiv ==> equiv ==> equiv) (iprod.iprod_insert x)
     iprod.iprod_lookup_insert:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
       EqDecision A → ∀ (f : iprod.iprod B) (x : A) (y : B x), iprod.iprod_insert x y f x = y
     iprod.iprod_lookup_insert_ne:
    -  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT) (f : iprod.iprod B) 
    -  (x x' : A) (y : B x), x ≠ x' → iprod.iprod_insert x y f x' = f x'
    +  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
    +  EqDecision A → ∀ (f : iprod.iprod B) (x x' : A) (y : B x), x ≠ x' → iprod.iprod_insert x y f x' = f x'
     iprod.iprod_lookup_timeless:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
       EqDecision A → ∀ (f : iprod.iprod B) (x : A), Timeless f → Timeless (f x)
    @@ -20360,8 +20481,10 @@
     NoDup_list_intersection:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (l k : list A), NoDup l → NoDup (list_intersection l k)
     elem_of_list_intersection_with:
    -  ∀ (A : Type) (f : A → A → option A) (l k : list A) (x : A),
    -  x ∈ list_intersection_with f l k ↔ (∃ x1 x2 : A, x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x)
    +  ∀ A : Type,
    +  EqDecision A
    +  → ∀ (f : A → A → option A) (l k : list A) (x : A),
    +    x ∈ list_intersection_with f l k ↔ (∃ x1 x2 : A, x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x)
     elem_of_list_filter:
       ∀ (A : Type) (P : A → Prop) (H : ∀ x : A, Decision (P x)) (l : list A) (x : A), x ∈ filter P l ↔ P x ∧ x ∈ l
     NoDup_filter: ∀ (A : Type) (P : A → Prop) (H : ∀ x : A, Decision (P x)) (l : list A), NoDup l → NoDup (filter P l)
    @@ -20818,7 +20941,7 @@
       ∀ (A : Type) (P : A → Prop) (l : list A) (i : nat) (k : list A),
       Forall P l → Forall P k → Forall P (list_inserts i k l)
     Forall_replicate: ∀ (A : Type) (P : A → Prop) (n : nat) (x : A), P x → Forall P (replicate n x)
    -Forall_replicate_eq: ∀ (A : Type) (n : nat) (x : A), Forall (eq x) (replicate n x)
    +Forall_replicate_eq: ∀ A : Type, (A → Prop) → ∀ (n : nat) (x : A), Forall (eq x) (replicate n x)
     Forall_take: ∀ (A : Type) (P : A → Prop) (n : nat) (l : list A), Forall P l → Forall P (take n l)
     Forall_drop: ∀ (A : Type) (P : A → Prop) (n : nat) (l : list A), Forall P l → Forall P (drop n l)
     Forall_resize:
    @@ -21118,32 +21241,47 @@
       Forall3 P l k k'
       → (∀ (x : A) (y : B) (z : C), l !! i = Some x → k !! i = Some y → k' !! i = Some z → P x y z → P (f x) (g y) z)
         → Forall3 P (alter f i l) (alter g i k) k'
    -equiv_Forall2: ∀ (A : Type) (H : Equiv A) (l k : list A), l ≡ k ↔ Forall2 equiv l k
    -list_equiv_lookup: ∀ (A : Type) (H : Equiv A) (l k : list A), l ≡ k ↔ (∀ i : nat, l !! i ≡ k !! i)
    +equiv_Forall2:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ l k : list A, l ≡ k ↔ Forall2 equiv l k
    +list_equiv_lookup:
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A) → ∀ l k : list A, l ≡ k ↔ (∀ i : nat, l !! i ≡ k !! i)
     list_equivalence:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Equivalence (equiv : relation (list A))
     list_leibniz:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → LeibnizEquiv A → LeibnizEquiv (list A)
    -cons_proper: ∀ (A : Type) (H : Equiv A), Proper (equiv ==> equiv ==> equiv) cons
    -app_proper: ∀ (A : Type) (H : Equiv A), Proper (equiv ==> equiv ==> equiv) app
    -length_proper: ∀ (A : Type) (H : Equiv A), Proper (equiv ==> eq) length
    +cons_proper:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv ==> equiv) cons
    +app_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv ==> equiv) app
    +length_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> eq) length
     tail_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv) tail
    -take_proper: ∀ (A : Type) (H : Equiv A) (n : nat), Proper (equiv ==> equiv) (take n)
    -drop_proper: ∀ (A : Type) (H : Equiv A) (n : nat), Proper (equiv ==> equiv) (drop n)
    +take_proper:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ n : nat, Proper (equiv ==> equiv) (take n)
    +drop_proper:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ n : nat, Proper (equiv ==> equiv) (drop n)
     list_lookup_proper:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ i : nat, Proper (equiv ==> equiv) (lookup i)
     list_alter_proper:
    -  ∀ (A : Type) (H : Equiv A) (f : A → A) (i : nat),
    -  Proper (equiv ==> equiv) f → Proper (equiv ==> equiv) (alter f i)
    -list_insert_proper: ∀ (A : Type) (H : Equiv A) (i : nat), Proper (equiv ==> equiv ==> equiv) (insert i)
    -list_inserts_proper: ∀ (A : Type) (H : Equiv A) (i : nat), Proper (equiv ==> equiv ==> equiv) (list_inserts i)
    -list_delete_proper: ∀ (A : Type) (H : Equiv A) (i : nat), Proper (equiv ==> equiv) (delete i)
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A)
    +  → ∀ (f : A → A) (i : nat), Proper (equiv ==> equiv) f → Proper (equiv ==> equiv) (alter f i)
    +list_insert_proper:
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A) → ∀ i : nat, Proper (equiv ==> equiv ==> equiv) (insert i)
    +list_inserts_proper:
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A) → ∀ i : nat, Proper (equiv ==> equiv ==> equiv) (list_inserts i)
    +list_delete_proper:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ i : nat, Proper (equiv ==> equiv) (delete i)
     option_list_proper:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv) option_list
     list_filter_proper:
    -  ∀ (A : Type) (H : Equiv A) (P : A → Prop) (H0 : ∀ x : A, Decision (P x)),
    -  Proper (equiv ==> iff) P → Proper (equiv ==> equiv) (filter P)
    -replicate_proper: ∀ (A : Type) (H : Equiv A) (n : nat), Proper (equiv ==> equiv) (replicate n)
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A)
    +  → ∀ (P : A → Prop) (H0 : ∀ x : A, Decision (P x)),
    +    Proper (equiv ==> iff) P → Proper (equiv ==> equiv) (filter P)
    +replicate_proper:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ n : nat, Proper (equiv ==> equiv) (replicate n)
     reverse_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv) reverse
     last_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv) last
     resize_proper:
    @@ -21963,19 +22101,28 @@
       Cofe B
       → Inhabited B → ∀ fB : A → B → B, (∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) → A → B
     fixpoint_AB_contractive:
    -  ∀ (A B : ofeT) (H0 : Cofe B) (Inhabited1 : Inhabited B) (fB : A → B → B)
    -  (H2 : ∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) (n : nat),
    -  Proper (dist_later n ==> dist n) (ofe.fixpoint_AB fB)
    +  ∀ A : ofeT,
    +  Cofe A
    +  → ∀ (B : ofeT) (H0 : Cofe B),
    +    Inhabited A
    +    → ∀ (Inhabited1 : Inhabited B) (fA : A → B → A) (fB : A → B → B),
    +      (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    +      → ∀ (H2 : ∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) (n : nat),
    +        Proper (dist_later n ==> dist n) (ofe.fixpoint_AB fB)
     ofe.fixpoint_AA:
       ∀ A B : ofeT,
       Cofe B
       → Inhabited B
         → (A → B → A) → ∀ fB : A → B → B, (∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) → A → A
     fixpoint_AA_contractive:
    -  ∀ (A B : ofeT) (H0 : Cofe B) (Inhabited1 : Inhabited B) (fA : A → B → A) (fB : A → B → B),
    -  (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    -  → ∀ (H2 : ∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) (n : nat),
    -    Proper (dist_later n ==> dist n) (ofe.fixpoint_AA fA fB)
    +  ∀ A : ofeT,
    +  Cofe A
    +  → ∀ (B : ofeT) (H0 : Cofe B),
    +    Inhabited A
    +    → ∀ (Inhabited1 : Inhabited B) (fA : A → B → A) (fB : A → B → B),
    +      (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    +      → ∀ (H2 : ∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) (n : nat),
    +        Proper (dist_later n ==> dist n) (ofe.fixpoint_AA fA fB)
     fixpoint_A:
       ∀ A : ofeT,
       Cofe A
    @@ -22007,11 +22154,27 @@
       (H2 : ∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB),
       fB (fixpoint_A fA fB) (fixpoint_B fA fB) ≡ fixpoint_B fA fB
     Proper_instance_0:
    -  ∀ (A B : ofeT) (fA : A → B → A),
    -  (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA) → Proper (equiv ==> equiv ==> equiv) fA
    +  ∀ A : ofeT,
    +  Cofe A
    +  → ∀ B : ofeT,
    +    Cofe B
    +    → Inhabited A
    +      → Inhabited B
    +        → ∀ (fA : A → B → A) (fB : A → B → B),
    +          (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    +          → (∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB)
    +            → Proper (equiv ==> equiv ==> equiv) fA
     Proper_instance_1:
    -  ∀ (A B : ofeT) (fB : A → B → B),
    -  (∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) → Proper (equiv ==> equiv ==> equiv) fB
    +  ∀ A : ofeT,
    +  Cofe A
    +  → ∀ B : ofeT,
    +    Cofe B
    +    → Inhabited A
    +      → Inhabited B
    +        → ∀ (fA : A → B → A) (fB : A → B → B),
    +          (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    +          → (∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB)
    +            → Proper (equiv ==> equiv ==> equiv) fB
     fixpoint_A_unique:
       ∀ (A : ofeT) (H : Cofe A) (B : ofeT) (H0 : Cofe B) (Inhabited0 : Inhabited A) (Inhabited1 : Inhabited B)
       (fA : A → B → A) (fB : A → B → B) (H1 : ∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    @@ -22656,27 +22819,35 @@
     option_Forall2_trans: ∀ (A : Type) (R : relation A), Transitive R → Transitive (option_Forall2 R)
     option_Forall2_equiv: ∀ (A : Type) (R : relation A), Equivalence R → Equivalence (option_Forall2 R)
     option_equiv: ∀ A : Type, Equiv A → Equiv (option A)
    -equiv_option_Forall2: ∀ (A : Type) (H : Equiv A) (mx my : option A), mx ≡ my ↔ option_Forall2 equiv mx my
    +equiv_option_Forall2:
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A) → ∀ mx my : option A, mx ≡ my ↔ option_Forall2 equiv mx my
     option_equivalence:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Equivalence (equiv : relation (option A))
    -Some_proper: ∀ (A : Type) (H : Equiv A), Proper (equiv ==> equiv) Some
    -Some_equiv_inj: ∀ (A : Type) (H : Equiv A), Inj equiv equiv Some
    +Some_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv) Some
    +Some_equiv_inj: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Inj equiv equiv Some
     option_leibniz:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → LeibnizEquiv A → LeibnizEquiv (option A)
     equiv_None: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ mx : option A, mx ≡ None ↔ mx = None
     equiv_Some_inv_l:
    -  ∀ (A : Type) (H : Equiv A) (mx my : option A) (x : A), mx ≡ my → mx = Some x → ∃ y : A, my = Some y ∧ x ≡ y
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A)
    +  → ∀ (mx my : option A) (x : A), mx ≡ my → mx = Some x → ∃ y : A, my = Some y ∧ x ≡ y
     equiv_Some_inv_r:
    -  ∀ (A : Type) (H : Equiv A) (mx my : option A) (y : A), mx ≡ my → my = Some y → ∃ x : A, mx = Some x ∧ x ≡ y
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A)
    +  → ∀ (mx my : option A) (y : A), mx ≡ my → my = Some y → ∃ x : A, mx = Some x ∧ x ≡ y
     equiv_Some_inv_l':
    -  ∀ (A : Type) (H : Equiv A) (my : option A) (x : A), Some x ≡ my → ∃ x' : A, Some x' = my ∧ x ≡ x'
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A) → ∀ (my : option A) (x : A), Some x ≡ my → ∃ x' : A, Some x' = my ∧ x ≡ x'
     equiv_Some_inv_r':
       ∀ (A : Type) (H : Equiv A),
       Equivalence (equiv : relation A) → ∀ (mx : option A) (y : A), mx ≡ Some y → ∃ y' : A, mx = Some y' ∧ y ≡ y'
    -is_Some_proper: ∀ (A : Type) (H : Equiv A), Proper (equiv ==> iff) is_Some
    +is_Some_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> iff) is_Some
     from_option_proper:
    -  ∀ (A : Type) (H : Equiv A) (B : Type) (R : relation B) (f : A → B),
    -  Proper (equiv ==> R) f → Proper (R ==> equiv ==> R) (from_option f)
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A)
    +  → ∀ (B : Type) (R : relation B) (f : A → B), Proper (equiv ==> R) f → Proper (R ==> equiv ==> R) (from_option f)
     option_eq_None_dec: ∀ (A : Type) (mx : option A), Decision (mx = None)
     option_None_eq_dec: ∀ (A : Type) (mx : option A), Decision (None = mx)
     option_eq_dec: ∀ A : Type, EqDecision A → EqDecision (option A)
    @@ -23578,16 +23749,22 @@
     sts_ctx:
       ∀ Σ : gFunctors, invG Σ → ∀ sts : stsT, stsG Σ sts → gname → namespace → (sts.state sts → iProp Σ) → iProp Σ
     sts_inv_ne:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (n : nat),
    -  Proper (pointwise_relation (sts.state sts) (dist n) ==> dist n) (sts_inv γ)
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (n : nat),
    +    Proper (pointwise_relation (sts.state sts) (dist n) ==> dist n) (sts_inv γ)
     sts_inv_proper:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname),
    -  Proper (pointwise_relation (sts.state sts) equiv ==> equiv) (sts_inv γ)
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname),
    +    Proper (pointwise_relation (sts.state sts) equiv ==> equiv) (sts_inv γ)
     sts_ownS_proper:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname), Proper (equiv ==> equiv ==> equiv) (sts_ownS γ)
    +  ∀ Σ : gFunctors,
    +  invG Σ → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname), Proper (equiv ==> equiv ==> equiv) (sts_ownS γ)
     sts_own_proper:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (s : sts.state sts),
    -  Proper (equiv ==> equiv) (sts_own γ s)
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (s : sts.state sts), Proper (equiv ==> equiv) (sts_own γ s)
     sts_ctx_ne:
       ∀ (Σ : gFunctors) (H : invG Σ) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (n : nat) 
       (N : namespace), Proper (pointwise_relation (sts.state sts) (dist n) ==> dist n) (sts_ctx γ N)
    @@ -23598,24 +23775,38 @@
       ∀ (Σ : gFunctors) (H : invG Σ) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (N : namespace)
       (φ : sts.state sts → iProp Σ), PersistentP (sts_ctx γ N φ)
     sts_own_peristent:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (s : sts.state sts), PersistentP (sts_own γ s ∅)
    +  ∀ Σ : gFunctors,
    +  invG Σ → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (s : sts.state sts), PersistentP (sts_own γ s ∅)
     sts_ownS_peristent:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (S : sts.states sts), PersistentP (sts_ownS γ S ∅)
    +  ∀ Σ : gFunctors,
    +  invG Σ → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (S : sts.states sts), PersistentP (sts_ownS γ S ∅)
     Params_instance_0: Params (@sts_inv) 4
     Params_instance_1: Params (@sts_ownS) 4
     Params_instance_2: Params (@sts_own) 5
     Params_instance_3: Params (@sts_ctx) 6
     sts_ownS_weaken:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (S1 S2 : sts.states sts) 
    -  (T1 T2 : sts.tokens sts), T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 → sts_ownS γ S1 T1 -∗ |==> sts_ownS γ S2 T2
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts),
    +    (sts.state sts → iProp Σ)
    +    → ∀ (γ : gname) (S1 S2 : sts.states sts) (T1 T2 : sts.tokens sts),
    +      T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 → sts_ownS γ S1 T1 -∗ |==> sts_ownS γ S2 T2
     sts_own_weaken:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (s : sts.state sts) (S : sts.states sts)
    -  (T1 T2 : sts.tokens sts), T2 ⊆ T1 → s ∈ S → sts.closed S T2 → sts_own γ s T1 -∗ |==> sts_ownS γ S T2
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts),
    +    (sts.state sts → iProp Σ)
    +    → ∀ (γ : gname) (s : sts.state sts) (S : sts.states sts) (T1 T2 : sts.tokens sts),
    +      T2 ⊆ T1 → s ∈ S → sts.closed S T2 → sts_own γ s T1 -∗ |==> sts_ownS γ S T2
     sts_ownS_op:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (S1 S2 : sts.states sts) 
    -  (T1 T2 : sts.tokens sts),
    -  T1 ⊥ T2
    -  → sts.closed S1 T1 → sts.closed S2 T2 → sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ∗ sts_ownS γ S2 T2)%I
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts),
    +    (sts.state sts → iProp Σ)
    +    → ∀ (γ : gname) (S1 S2 : sts.states sts) (T1 T2 : sts.tokens sts),
    +      T1 ⊥ T2
    +      → sts.closed S1 T1
    +        → sts.closed S2 T2 → sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ∗ sts_ownS γ S2 T2)%I
     sts_alloc:
       ∀ (Σ : gFunctors) (H : invG Σ) (sts : stsT) (H0 : stsG Σ sts) (φ : sts.state sts → iProp Σ) 
       (E : coPset) (N : namespace) (s : sts.state sts),
    @@ -23708,7 +23899,8 @@
       CMRATotal A
       → CMRADiscrete A → ∀ (x : A) (P : A → Prop), x ~~>: P ↔ (∀ z : A, ✓ (x ⋅ z) → ∃ y : A, P y ∧ ✓ (y ⋅ z))
     cmra_discrete_update:
    -  ∀ A : cmraT, CMRATotal A → CMRADiscrete A → ∀ x y : A, x ~~> y ↔ (∀ z : A, ✓ (x ⋅ z) → ✓ (y ⋅ z))
    +  ∀ A : cmraT,
    +  CMRATotal A → CMRADiscrete A → CMRADiscrete A → ∀ x y : A, x ~~> y ↔ (∀ z : A, ✓ (x ⋅ z) → ✓ (y ⋅ z))
     cmra_transport_updateP:
       ∀ (A B : cmraT) (H : A = B) (P : A → Prop) (Q : B → Prop) (x : A),
       x ~~>: P → (∀ y : A, P y → Q (cmra_transport H y)) → cmra_transport H x ~~>: Q
    @@ -24042,8 +24234,7 @@
     wsat.ownD: ∀ Σ : gFunctors, invG Σ → gset positive → iProp Σ
     wsat.Params_instance_2: Params (@wsat.ownD) 3
     wsat.wsat: ∀ Σ : gFunctors, invG Σ → iProp Σ
    -wsat.invariant_unfold_contractive:
    -  ∀ (Σ : gFunctors) (n : nat), Proper (dist_later n ==> dist n) wsat.invariant_unfold
    +wsat.invariant_unfold_contractive: ∀ Σ : gFunctors, invG Σ → Contractive wsat.invariant_unfold
     wsat.ownI_contractive:
       ∀ (Σ : gFunctors) (H : invG Σ) (i : positive) (n : nat), Proper (dist_later n ==> dist n) (wsat.ownI i)
     wsat.ownI_persistent: ∀ (Σ : gFunctors) (H : invG Σ) (i : positive) (P : iProp Σ), PersistentP (wsat.ownI i P)
    @@ -32691,7 +32882,9 @@
     sel_patterns.sel_pat.parse: string → list sel_patterns.sel_pat
     cofe_solver.solver.A: cFunctor → nat → ofeT
     cofe_solver.solver.Cofe_instance_0:
    -  ∀ F : cFunctor, (∀ T : ofeT, Cofe T → Cofe (F T)) → ∀ k : nat, Cofe (cofe_solver.solver.A F k)
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T)) → Inhabited (F unitC) → ∀ k : nat, Cofe (cofe_solver.solver.A F k)
     cofe_solver.solver.f:
       ∀ F : cFunctor, Inhabited (F unitC) → ∀ k : nat, cofe_solver.solver.A F k -n> cofe_solver.solver.A F (S k)
     cofe_solver.solver.g:
    @@ -32705,13 +32898,15 @@
     cofe_solver.solver.gf:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F k),
    -    (cofe_solver.solver.g F k) ((cofe_solver.solver.f F k) x) ≡ x
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.g F k) ((cofe_solver.solver.f F k) x) ≡ x
     cofe_solver.solver.fg:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F (S (S k))),
    -    (cofe_solver.solver.f F (S k)) ((cofe_solver.solver.g F (S k)) x) ≡{k}≡ x
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F (S (S k))),
    +      (cofe_solver.solver.f F (S k)) ((cofe_solver.solver.g F (S k)) x) ≡{k}≡ x
     cofe_solver.solver.tower: ∀ F : cFunctor, Inhabited (F unitC) → Type
     cofe_solver.solver.Build_tower:
       ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (tower_car : ∀ k : nat, cofe_solver.solver.A F k),
    @@ -32724,17 +32919,21 @@
     cofe_solver.solver.tower_equiv: ∀ (F : cFunctor) (Finh : Inhabited (F unitC)), Equiv (cofe_solver.solver.tower F)
     cofe_solver.solver.tower_dist: ∀ (F : cFunctor) (Finh : Inhabited (F unitC)), Dist (cofe_solver.solver.tower F)
     cofe_solver.solver.tower_ofe_mixin:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)), OfeMixin (cofe_solver.solver.tower F)
    -cofe_solver.solver.T: ∀ F : cFunctor, Inhabited (F unitC) → ofeT
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T)) → ∀ Finh : Inhabited (F unitC), OfeMixin (cofe_solver.solver.tower F)
    +cofe_solver.solver.T:
    +  ∀ F : cFunctor, cFunctorContractive F → (∀ T : ofeT, Cofe T → Cofe (F T)) → Inhabited (F unitC) → ofeT
     cofe_solver.solver.tower_chain_obligation_1:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (c : chain (cofe_solver.solver.T F)) (k n i : nat),
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (c : chain (cofe_solver.solver.T F)) (k n i : nat),
       (n ≤ i)%nat → (c i) k ≡{n}≡ (c n) k
     cofe_solver.solver.tower_chain:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)),
    -  chain (cofe_solver.solver.T F) → ∀ k : nat, chain (cofe_solver.solver.A F k)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), chain (cofe_solver.solver.T F) → ∀ k : nat, chain (cofe_solver.solver.A F k)
     cofe_solver.solver.tower_compl_obligation_1:
    -  ∀ (F : cFunctor) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T)) (Finh : Inhabited (F unitC))
    -  (c : chain (cofe_solver.solver.T F)) (k : nat)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (c : chain (cofe_solver.solver.T F)) (k : nat)
       (H:=
        (λ x y : cofe_solver.solver.A F k, match equiv_dist x y with
                                           | conj _ x1 => x1
    @@ -32743,15 +32942,15 @@
       (cofe_solver.solver.g F k) (compl (cofe_solver.solver.tower_chain F c (S k)))
       ≡ compl (cofe_solver.solver.tower_chain F c k)
     cofe_solver.solver.tower_compl:
    -  ∀ F : cFunctor,
    -  (∀ T : ofeT, Cofe T → Cofe (F T))
    -  → ∀ Finh : Inhabited (F unitC), chain (cofe_solver.solver.T F) → cofe_solver.solver.T F
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), chain (cofe_solver.solver.T F) → cofe_solver.solver.T F
     cofe_solver.solver.tower_cofe_obligation_1:
    -  ∀ (F : cFunctor) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T)) (Finh : Inhabited (F unitC)) 
    -  (n : nat) (c : chain (cofe_solver.solver.T F)), cofe_solver.solver.tower_compl F c ≡{n}≡ 
    -  c n
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (n : nat) (c : chain (cofe_solver.solver.T F)),
    +  cofe_solver.solver.tower_compl F c ≡{n}≡ c n
     cofe_solver.solver.tower_cofe:
    -  ∀ F : cFunctor, (∀ T : ofeT, Cofe T → Cofe (F T)) → ∀ Finh : Inhabited (F unitC), Cofe (cofe_solver.solver.T F)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), Cofe (cofe_solver.solver.T F)
     cofe_solver.solver.ff:
       ∀ F : cFunctor, Inhabited (F unitC) → ∀ k i : nat, cofe_solver.solver.A F k -n> cofe_solver.solver.A F (i + k)
     cofe_solver.solver.gg:
    @@ -32759,89 +32958,120 @@
     cofe_solver.solver.ggff:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (x : cofe_solver.solver.A F k),
    -    (cofe_solver.solver.gg F i) ((cofe_solver.solver.ff F i) x) ≡ x
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.gg F i) ((cofe_solver.solver.ff F i) x) ≡ x
     cofe_solver.solver.f_tower:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat) (X : cofe_solver.solver.tower F),
    -    (cofe_solver.solver.f F (S k)) (X (S k)) ≡{k}≡ X (S (S k))
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k : nat) (X : cofe_solver.solver.tower F),
    +      (cofe_solver.solver.f F (S k)) (X (S k)) ≡{k}≡ X (S (S k))
     cofe_solver.solver.ff_tower:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (X : cofe_solver.solver.tower F),
    -    (cofe_solver.solver.ff F i) (X (S k)) ≡{k}≡ X (i + S k)%nat
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (X : cofe_solver.solver.tower F),
    +      (cofe_solver.solver.ff F i) (X (S k)) ≡{k}≡ X (i + S k)%nat
     cofe_solver.solver.gg_tower:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k i : nat) (X : cofe_solver.solver.tower F),
    -  (cofe_solver.solver.gg F i) (X (i + k)%nat) ≡ X k
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (X : cofe_solver.solver.tower F),
    +      (cofe_solver.solver.gg F i) (X (i + k)%nat) ≡ X k
     cofe_solver.solver.tower_car_ne:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (n k : nat),
    -  Proper (dist n ==> dist n) (λ X : cofe_solver.solver.tower F, X k)
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (n k : nat),
    +      Proper (dist n ==> dist n) (λ X : cofe_solver.solver.tower F, X k)
     cofe_solver.solver.project:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.T F -n> cofe_solver.solver.A F k
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.T F -n> cofe_solver.solver.A F k
     cofe_solver.solver.coerce:
       ∀ (F : cFunctor) (i j : nat), i = j → cofe_solver.solver.A F i -n> cofe_solver.solver.A F j
     cofe_solver.solver.coerce_id:
    -  ∀ (F : cFunctor) (i : nat) (H : i = i) (x : cofe_solver.solver.A F i), (cofe_solver.solver.coerce F H) x = x
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → Inhabited (F unitC)
    +      → ∀ (i : nat) (H : i = i) (x : cofe_solver.solver.A F i), (cofe_solver.solver.coerce F H) x = x
     cofe_solver.solver.coerce_proper:
    -  ∀ (F : cFunctor) (i j : nat) (x y : cofe_solver.solver.A F i) (H1 H2 : i = j),
    -  x = y → (cofe_solver.solver.coerce F H1) x = (cofe_solver.solver.coerce F H2) y
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → Inhabited (F unitC)
    +      → ∀ (i j : nat) (x y : cofe_solver.solver.A F i) (H1 H2 : i = j),
    +        x = y → (cofe_solver.solver.coerce F H1) x = (cofe_solver.solver.coerce F H2) y
     cofe_solver.solver.g_coerce:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k j : nat) (H : S k = S j) (x : cofe_solver.solver.A F (S k)),
    -  (cofe_solver.solver.g F j) ((cofe_solver.solver.coerce F H) x) =
    -  (cofe_solver.solver.coerce F (Nat.succ_inj k j H)) ((cofe_solver.solver.g F k) x)
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k j : nat) (H : S k = S j) (x : cofe_solver.solver.A F (S k)),
    +      (cofe_solver.solver.g F j) ((cofe_solver.solver.coerce F H) x) =
    +      (cofe_solver.solver.coerce F (Nat.succ_inj k j H)) ((cofe_solver.solver.g F k) x)
     cofe_solver.solver.coerce_f:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k j : nat) (H : S k = S j) (x : cofe_solver.solver.A F k),
    -  (cofe_solver.solver.coerce F H) ((cofe_solver.solver.f F k) x) =
    -  (cofe_solver.solver.f F j) ((cofe_solver.solver.coerce F (Nat.succ_inj k j H)) x)
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k j : nat) (H : S k = S j) (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.coerce F H) ((cofe_solver.solver.f F k) x) =
    +      (cofe_solver.solver.f F j) ((cofe_solver.solver.coerce F (Nat.succ_inj k j H)) x)
     cofe_solver.solver.gg_gg:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k i i1 i2 j : nat) (H1 : k = (i + j)%nat)
    -  (H2 : k = (i2 + (i1 + j))%nat) (x : cofe_solver.solver.A F k),
    -  (cofe_solver.solver.gg F i) ((cofe_solver.solver.coerce F H1) x) =
    -  (cofe_solver.solver.gg F i1) ((cofe_solver.solver.gg F i2) ((cofe_solver.solver.coerce F H2) x))
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i i1 i2 j : nat) (H1 : k = (i + j)%nat) (H2 : k = (i2 + (i1 + j))%nat)
    +      (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.gg F i) ((cofe_solver.solver.coerce F H1) x) =
    +      (cofe_solver.solver.gg F i1) ((cofe_solver.solver.gg F i2) ((cofe_solver.solver.coerce F H2) x))
     cofe_solver.solver.ff_ff:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k i i1 i2 j : nat) (H1 : (i + k)%nat = j)
    -  (H2 : (i1 + (i2 + k))%nat = j) (x : cofe_solver.solver.A F k),
    -  (cofe_solver.solver.coerce F H1) ((cofe_solver.solver.ff F i) x) =
    -  (cofe_solver.solver.coerce F H2) ((cofe_solver.solver.ff F i1) ((cofe_solver.solver.ff F i2) x))
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i i1 i2 j : nat) (H1 : (i + k)%nat = j) (H2 : (i1 + (i2 + k))%nat = j)
    +      (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.coerce F H1) ((cofe_solver.solver.ff F i) x) =
    +      (cofe_solver.solver.coerce F H2) ((cofe_solver.solver.ff F i1) ((cofe_solver.solver.ff F i2) x))
     cofe_solver.solver.embed_coerce:
       ∀ F : cFunctor, Inhabited (F unitC) → ∀ k i : nat, cofe_solver.solver.A F k -n> cofe_solver.solver.A F i
     cofe_solver.solver.g_embed_coerce:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (x : cofe_solver.solver.A F k),
    -    (cofe_solver.solver.g F i) ((cofe_solver.solver.embed_coerce F (S i)) x)
    -    ≡ (cofe_solver.solver.embed_coerce F i) x
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.g F i) ((cofe_solver.solver.embed_coerce F (S i)) x)
    +      ≡ (cofe_solver.solver.embed_coerce F i) x
     cofe_solver.solver.embed_obligation_1:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F k) (i : nat),
    -    (cofe_solver.solver.g F i) ((cofe_solver.solver.embed_coerce F (S i)) x)
    -    ≡ (cofe_solver.solver.embed_coerce F i) x
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F k) (i : nat),
    +      (cofe_solver.solver.g F i) ((cofe_solver.solver.embed_coerce F (S i)) x)
    +      ≡ (cofe_solver.solver.embed_coerce F i) x
     cofe_solver.solver.embed:
    -  ∀ F : cFunctor,
    -  cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.A F k → cofe_solver.solver.T F
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.A F k → cofe_solver.solver.T F
     cofe_solver.solver.Params_instance_0:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)),
    -  Params (cofe_solver.solver.embed F) 1
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), Params (cofe_solver.solver.embed F) 1
     cofe_solver.solver.embed_ne:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (k n : nat),
    -  Proper (dist n ==> dist n) (cofe_solver.solver.embed F k)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k n : nat), Proper (dist n ==> dist n) (cofe_solver.solver.embed F k)
     cofe_solver.solver.embed':
    -  ∀ F : cFunctor,
    -  cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.A F k -n> cofe_solver.solver.T F
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.A F k -n> cofe_solver.solver.T F
     cofe_solver.solver.embed_f:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (k : nat)
    -  (x : cofe_solver.solver.A F k),
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F k),
       cofe_solver.solver.embed F (S k) ((cofe_solver.solver.f F k) x) ≡ cofe_solver.solver.embed F k x
     cofe_solver.solver.embed_tower:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (k : nat)
    -  (X : cofe_solver.solver.T F), cofe_solver.solver.embed F (S k) (X (S k)) ≡{k}≡ X
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k : nat) (X : cofe_solver.solver.T F),
    +  cofe_solver.solver.embed F (S k) (X (S k)) ≡{k}≡ X
     cofe_solver.solver.unfold_chain_obligation_1:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (X : cofe_solver.solver.T F)
    -  (n i : nat) (Hi : (n ≤ i)%nat)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (X : cofe_solver.solver.T F) (n i : nat) (Hi : (n ≤ i)%nat)
       (H:=
        ex_intro (λ k : nat, i = (k + n)%nat) (i - n)%nat
          (Nat2Z.inj i (i - n + n)
    @@ -32931,31 +33161,28 @@
       (cFunctor_map F (cofe_solver.solver.project F i, cofe_solver.solver.embed' F i)) (X (S i)) ≡{n}≡ 
       (cFunctor_map F (cofe_solver.solver.project F n, cofe_solver.solver.embed' F n)) (X (S n))
     cofe_solver.solver.unfold_chain:
    -  ∀ F : cFunctor,
    -  cFunctorContractive F
    -  → ∀ Finh : Inhabited (F unitC), cofe_solver.solver.T F → chain (F (cofe_solver.solver.T F))
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), cofe_solver.solver.T F → chain (F (cofe_solver.solver.T F))
     cofe_solver.solver.unfold:
    -  ∀ F : cFunctor,
    -  cFunctorContractive F
    -  → (∀ T : ofeT, Cofe T → Cofe (F T))
    -    → ∀ Finh : Inhabited (F unitC), cofe_solver.solver.T F → F (cofe_solver.solver.T F)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), cofe_solver.solver.T F → F (cofe_solver.solver.T F)
     cofe_solver.solver.unfold_ne:
       ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
       (Finh : Inhabited (F unitC)) (n : nat), Proper (dist n ==> dist n) (cofe_solver.solver.unfold F)
     cofe_solver.solver.fold_obligation_1:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (X : F (cofe_solver.solver.T F))
    -  (k : nat),
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (X : F (cofe_solver.solver.T F)) (k : nat),
       (cofe_solver.solver.g F k)
         ((cofe_solver.solver.g F (S k))
            ((cFunctor_map F (cofe_solver.solver.embed' F (S k), cofe_solver.solver.project F (S k))) X))
       ≡ (cofe_solver.solver.g F k)
           ((cFunctor_map F (cofe_solver.solver.embed' F k, cofe_solver.solver.project F k)) X)
     cofe_solver.solver.fold:
    -  ∀ F : cFunctor,
    -  cFunctorContractive F → ∀ Finh : Inhabited (F unitC), F (cofe_solver.solver.T F) → cofe_solver.solver.T F
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), F (cofe_solver.solver.T F) → cofe_solver.solver.T F
     cofe_solver.solver.fold_ne:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (n : nat),
    -  Proper (dist n ==> dist n) (cofe_solver.solver.fold F)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (n : nat), Proper (dist n ==> dist n) (cofe_solver.solver.fold F)
     cofe_solver.solver.result:
       ∀ F : cFunctor,
       cFunctorContractive F → (∀ T : ofeT, Cofe T → Cofe (F T)) → Inhabited (F unitC) → cofe_solver.solution F
    @@ -33694,15 +33921,17 @@
       (Φ : val → uPred (iResUR Σ)),
       True -∗ ▷ (∀ l : loc, recv N l P ∗ send N l P -∗ Φ #l) -∗ WP newbarrier #() {{ v, Φ v }}
     ress_split:
    -  ∀ (Σ : gFunctors) (barrierG0 : barrierG Σ) (i i1 i2 : gname) (Q R1 R2 : ∙%CF (iProp Σ)) 
    -  (P : iProp Σ) (I : gset gname),
    -  i ∈ I
    -  → i1 ∉ I
    -    → i2 ∉ I
    -      → i1 ≠ i2
    -        → saved_prop_own i Q -∗
    -          saved_prop_own i1 R1 -∗
    -          saved_prop_own i2 R2 -∗ (Q -∗ R1 ∗ R2) -∗ ress P I -∗ ress P ({[i1; i2]} ∪ I ∖ {[i]})
    +  ∀ Σ : gFunctors,
    +  heapG Σ
    +  → ∀ (barrierG0 : barrierG Σ) (i i1 i2 : gname) (Q R1 R2 : ∙%CF (iProp Σ)) (P : iProp Σ) 
    +    (I : gset gname),
    +    i ∈ I
    +    → i1 ∉ I
    +      → i2 ∉ I
    +        → i1 ≠ i2
    +          → saved_prop_own i Q -∗
    +            saved_prop_own i1 R1 -∗
    +            saved_prop_own i2 R2 -∗ (Q -∗ R1 ∗ R2) -∗ ress P I -∗ ress P ({[i1; i2]} ∪ I ∖ {[i]})
     recv_ne:
       ∀ (Σ : gFunctors) (heapG0 : heapG Σ) (barrierG0 : barrierG Σ) (N : namespace) (n : nat) 
       (l : loc), Proper (dist n ==> dist n) (recv N l)
    @@ -33715,8 +33944,9 @@
     barrier_inv_ne:
       ∀ (Σ : gFunctors) (heapG0 : heapG Σ) (barrierG0 : barrierG Σ) (n : nat) (l : loc),
       Proper (dist n ==> eq ==> dist n) (barrier_inv l)
    -state_to_prop_ne: ∀ (Σ : gFunctors) (n : nat) (s : state), Proper (dist n ==> dist n) (state_to_prop s)
    -ress_ne: ∀ (Σ : gFunctors) (barrierG0 : barrierG Σ) (n : nat), Proper (dist n ==> eq ==> dist n) ress
    +state_to_prop_ne:
    +  ∀ Σ : gFunctors, heapG Σ → barrierG Σ → ∀ (n : nat) (s : state), Proper (dist n ==> dist n) (state_to_prop s)
    +ress_ne: ∀ Σ : gFunctors, heapG Σ → ∀ (barrierG0 : barrierG Σ) (n : nat), Proper (dist n ==> eq ==> dist n) ress
     barrier_ctx_persistent:
       ∀ (Σ : gFunctors) (heapG0 : heapG Σ) (barrierG0 : barrierG Σ) (N : namespace) (γ : gname) 
       (l : loc) (P : iProp Σ), PersistentP (barrier_ctx N γ l P)
  • After removing "Proof Using" from three files, the diff got better:

    --- about-old	2017-01-04 13:30:17.753281969 +0100
    +++ about-new	2017-01-04 17:46:23.037587248 +0100
    @@ -12953,7 +12953,7 @@
     cmra_opM_assoc_L: ∀ A : cmraT, LeibnizEquiv A → ∀ (x y : A) (mz : option A), x ⋅ y ⋅? mz = x ⋅ (y ⋅? mz)
     cmra_pcore_r_L: ∀ A : cmraT, LeibnizEquiv A → ∀ x cx : A, pcore x = Some cx → x ⋅ cx = x
     cmra_pcore_dup_L: ∀ A : cmraT, LeibnizEquiv A → ∀ x cx : A, pcore x = Some cx → cx = cx ⋅ cx
    -persistent_dup_L: ∀ (A : cmraT) (x : A), Persistent x → x ≡ x ⋅ x
    +persistent_dup_L: ∀ A : cmraT, LeibnizEquiv A → ∀ x : A, Persistent x → x = x ⋅ x
     cmra_core_r_L: ∀ A : cmraT, LeibnizEquiv A → CMRATotal A → ∀ x : A, x ⋅ core x = x
     cmra_core_l_L: ∀ A : cmraT, LeibnizEquiv A → CMRATotal A → ∀ x : A, core x ⋅ x = x
     cmra_core_idemp_L: ∀ A : cmraT, LeibnizEquiv A → CMRATotal A → ∀ x : A, core (core x) = core x
    @@ -14276,10 +14276,10 @@
       (H4 : Difference C), Collection A C → LeibnizEquiv C → ∀ X Y Z : C, X ∩ Y ∪ Z = (X ∪ Z) ∩ (Y ∪ Z)
     intersection_union_l_L:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Intersection C)
    -  (H4 : Difference C), Collection A C → ∀ X Y Z : C, X ∩ (Y ∪ Z) ≡ X ∩ Y ∪ X ∩ Z
    +  (H4 : Difference C), Collection A C → LeibnizEquiv C → ∀ X Y Z : C, X ∩ (Y ∪ Z) = X ∩ Y ∪ X ∩ Z
     intersection_union_r_L:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Intersection C)
    -  (H4 : Difference C), Collection A C → ∀ X Y Z : C, (X ∪ Y) ∩ Z ≡ X ∩ Z ∪ Y ∩ Z
    +  (H4 : Difference C), Collection A C → LeibnizEquiv C → ∀ X Y Z : C, (X ∪ Y) ∩ Z = X ∩ Z ∪ Y ∩ Z
     difference_twice_L:
       ∀ (A C : Type) (H : ElemOf A C) (H0 : Empty C) (H1 : Singleton A C) (H2 : Union C) (H3 : Intersection C)
       (H4 : Difference C), Collection A C → LeibnizEquiv C → ∀ X Y : C, X ∖ Y ∖ Y = X ∖ Y
    @@ -15111,7 +15111,7 @@
         → ∀ p p0 : positive, choose_step P p p0 → P0 p p0
     choose_step_acc:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : Countable A) (P : A → Prop),
    -  (∃ x : A, P x) → Acc (choose_step P) 1%positive
    +  (∀ x : A, Decision (P x)) → (∃ x : A, P x) → Acc (choose_step P) 1%positive
     choose_go:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : Countable A) (P : A → Prop),
       (∀ x : A, Decision (P x)) → ∀ i : positive, Acc (choose_step P) i → A
    @@ -16972,8 +16972,9 @@
       (EqDecision0 : EqDecision K),
       FinMap K M → ∀ (A : Type) (H7 : Equiv A), Equivalence (equiv : relation A) → ∀ m : M A, m ≡ ∅ ↔ m = ∅
     map_equiv_lookup_l:
    -  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (H7 : Equiv A) 
    -  (m1 m2 : M A) (i : K) (x : A), m1 ≡ m2 → m1 !! i = Some x → ∃ y : A, m2 !! i = Some y ∧ x ≡ y
    +  ∀ (K : Type) (M : Type → Type) (H0 : ∀ A : Type, Lookup K A (M A)) (A : Type) (H7 : Equiv A),
    +  Equivalence (equiv : relation A)
    +  → ∀ (m1 m2 : M A) (i : K) (x : A), m1 ≡ m2 → m1 !! i = Some x → ∃ y : A, m2 !! i = Some y ∧ x ≡ y
     map_fmap_proper:
       ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : ∀ A : Type, Lookup K A (M A)) (H1 : ∀ A : Type, Empty (M A))
       (H2 : ∀ A : Type, PartialAlter K A (M A)) (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
    @@ -18396,10 +18397,10 @@
       (H0 : finite.Finite B) (f : A → B), Inj eq eq f → Surj eq f → finite.card A = finite.card B
     finite.Forall_finite:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (P : A → Prop),
    -  Forall P (finite.enum A) ↔ (∀ x : A, P x)
    +  (∀ x : A, Decision (P x)) → Forall P (finite.enum A) ↔ (∀ x : A, P x)
     finite.Exists_finite:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (P : A → Prop),
    -  Exists P (finite.enum A) ↔ (∃ x : A, P x)
    +  (∀ x : A, Decision (P x)) → Exists P (finite.enum A) ↔ (∃ x : A, P x)
     finite.forall_dec:
       ∀ (A : Type) (EqDecision0 : EqDecision A),
       finite.Finite A → ∀ P : A → Prop, (∀ x : A, Decision (P x)) → Decision (∀ x : A, P x)
    @@ -18894,15 +18895,19 @@
       FreshSpec K (gset K)
       → ∀ (m : gmap K A) (x : A), ✓ x → m ~~>: (λ m' : gmap K A, ∃ i : K, m' = <[i:=x]> m ∧ m !! i = None)
     gmap.alloc_unit_singleton_updateP:
    -  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (P : A → Prop) 
    -  (Q : gmap K A → Prop) (u : A) (i : K),
    -  ✓ u → LeftId equiv u op → u ~~>: P → (∀ y : A, P y → Q {[i := y]}) → ∅ ~~>: Q
    +  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (H0 : Fresh K (gset K)),
    +  FreshSpec K (gset K)
    +  → ∀ (P : A → Prop) (Q : gmap K A → Prop) (u : A) (i : K),
    +    ✓ u → LeftId equiv u op → u ~~>: P → (∀ y : A, P y → Q {[i := y]}) → ∅ ~~>: Q
     gmap.alloc_unit_singleton_updateP':
    -  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (P : A → Prop) 
    -  (u : A) (i : K), ✓ u → LeftId equiv u op → u ~~>: P → ∅ ~~>: (λ m : gmap K A, ∃ y : A, m = {[i := y]} ∧ P y)
    +  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (H0 : Fresh K (gset K)),
    +  FreshSpec K (gset K)
    +  → ∀ (P : A → Prop) (u : A) (i : K),
    +    ✓ u → LeftId equiv u op → u ~~>: P → ∅ ~~>: (λ m : gmap K A, ∃ y : A, m = {[i := y]} ∧ P y)
     gmap.alloc_unit_singleton_update:
    -  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (u : A) (i : K) 
    -  (y : A), ✓ u → LeftId equiv u op → u ~~> y → (∅ : gmap K A) ~~> {[i := y]}
    +  ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (H0 : Fresh K (gset K)),
    +  FreshSpec K (gset K)
    +  → ∀ (u : A) (i : K) (y : A), ✓ u → LeftId equiv u op → u ~~> y → (∅ : gmap K A) ~~> {[i := y]}
     gmap.alloc_local_update:
       ∀ (K : Type) (EqDecision0 : EqDecision K) (H : Countable K) (A : cmraT) (m1 m2 : gmap K A) 
       (i : K) (x : A), m1 !! i = None → ✓ x → local_updates.local_update (m1, m2) (<[i:=x]> m1, <[i:=x]> m2)
    @@ -19475,17 +19480,17 @@
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
       (∀ a : A, Cofe (B a)) → Cofe (iprod.iprodC B)
     iprod.iprod_insert_ne:
    -  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT) (n : nat) 
    -  (x : A), Proper (dist n ==> dist n ==> dist n) (iprod.iprod_insert x)
    +  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
    +  EqDecision A → ∀ (n : nat) (x : A), Proper (dist n ==> dist n ==> dist n) (iprod.iprod_insert x)
     iprod.iprod_insert_proper:
    -  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT) (x : A),
    -  Proper (equiv ==> equiv ==> equiv) (iprod.iprod_insert x)
    +  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
    +  EqDecision A → ∀ x : A, Proper (equiv ==> equiv ==> equiv) (iprod.iprod_insert x)
     iprod.iprod_lookup_insert:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
       EqDecision A → ∀ (f : iprod.iprod B) (x : A) (y : B x), iprod.iprod_insert x y f x = y
     iprod.iprod_lookup_insert_ne:
    -  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT) (f : iprod.iprod B) 
    -  (x x' : A) (y : B x), x ≠ x' → iprod.iprod_insert x y f x' = f x'
    +  ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
    +  EqDecision A → ∀ (f : iprod.iprod B) (x x' : A) (y : B x), x ≠ x' → iprod.iprod_insert x y f x' = f x'
     iprod.iprod_lookup_timeless:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (H : finite.Finite A) (B : A → ofeT),
       EqDecision A → ∀ (f : iprod.iprod B) (x : A), Timeless f → Timeless (f x)
    @@ -20360,8 +20365,10 @@
     NoDup_list_intersection:
       ∀ (A : Type) (EqDecision0 : EqDecision A) (l k : list A), NoDup l → NoDup (list_intersection l k)
     elem_of_list_intersection_with:
    -  ∀ (A : Type) (f : A → A → option A) (l k : list A) (x : A),
    -  x ∈ list_intersection_with f l k ↔ (∃ x1 x2 : A, x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x)
    +  ∀ A : Type,
    +  EqDecision A
    +  → ∀ (f : A → A → option A) (l k : list A) (x : A),
    +    x ∈ list_intersection_with f l k ↔ (∃ x1 x2 : A, x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x)
     elem_of_list_filter:
       ∀ (A : Type) (P : A → Prop) (H : ∀ x : A, Decision (P x)) (l : list A) (x : A), x ∈ filter P l ↔ P x ∧ x ∈ l
     NoDup_filter: ∀ (A : Type) (P : A → Prop) (H : ∀ x : A, Decision (P x)) (l : list A), NoDup l → NoDup (filter P l)
    @@ -20818,7 +20825,7 @@
       ∀ (A : Type) (P : A → Prop) (l : list A) (i : nat) (k : list A),
       Forall P l → Forall P k → Forall P (list_inserts i k l)
     Forall_replicate: ∀ (A : Type) (P : A → Prop) (n : nat) (x : A), P x → Forall P (replicate n x)
    -Forall_replicate_eq: ∀ (A : Type) (n : nat) (x : A), Forall (eq x) (replicate n x)
    +Forall_replicate_eq: ∀ A : Type, (A → Prop) → ∀ (n : nat) (x : A), Forall (eq x) (replicate n x)
     Forall_take: ∀ (A : Type) (P : A → Prop) (n : nat) (l : list A), Forall P l → Forall P (take n l)
     Forall_drop: ∀ (A : Type) (P : A → Prop) (n : nat) (l : list A), Forall P l → Forall P (drop n l)
     Forall_resize:
    @@ -21118,32 +21125,47 @@
       Forall3 P l k k'
       → (∀ (x : A) (y : B) (z : C), l !! i = Some x → k !! i = Some y → k' !! i = Some z → P x y z → P (f x) (g y) z)
         → Forall3 P (alter f i l) (alter g i k) k'
    -equiv_Forall2: ∀ (A : Type) (H : Equiv A) (l k : list A), l ≡ k ↔ Forall2 equiv l k
    -list_equiv_lookup: ∀ (A : Type) (H : Equiv A) (l k : list A), l ≡ k ↔ (∀ i : nat, l !! i ≡ k !! i)
    +equiv_Forall2:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ l k : list A, l ≡ k ↔ Forall2 equiv l k
    +list_equiv_lookup:
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A) → ∀ l k : list A, l ≡ k ↔ (∀ i : nat, l !! i ≡ k !! i)
     list_equivalence:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Equivalence (equiv : relation (list A))
     list_leibniz:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → LeibnizEquiv A → LeibnizEquiv (list A)
    -cons_proper: ∀ (A : Type) (H : Equiv A), Proper (equiv ==> equiv ==> equiv) cons
    -app_proper: ∀ (A : Type) (H : Equiv A), Proper (equiv ==> equiv ==> equiv) app
    -length_proper: ∀ (A : Type) (H : Equiv A), Proper (equiv ==> eq) length
    +cons_proper:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv ==> equiv) cons
    +app_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv ==> equiv) app
    +length_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> eq) length
     tail_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv) tail
    -take_proper: ∀ (A : Type) (H : Equiv A) (n : nat), Proper (equiv ==> equiv) (take n)
    -drop_proper: ∀ (A : Type) (H : Equiv A) (n : nat), Proper (equiv ==> equiv) (drop n)
    +take_proper:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ n : nat, Proper (equiv ==> equiv) (take n)
    +drop_proper:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ n : nat, Proper (equiv ==> equiv) (drop n)
     list_lookup_proper:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ i : nat, Proper (equiv ==> equiv) (lookup i)
     list_alter_proper:
    -  ∀ (A : Type) (H : Equiv A) (f : A → A) (i : nat),
    -  Proper (equiv ==> equiv) f → Proper (equiv ==> equiv) (alter f i)
    -list_insert_proper: ∀ (A : Type) (H : Equiv A) (i : nat), Proper (equiv ==> equiv ==> equiv) (insert i)
    -list_inserts_proper: ∀ (A : Type) (H : Equiv A) (i : nat), Proper (equiv ==> equiv ==> equiv) (list_inserts i)
    -list_delete_proper: ∀ (A : Type) (H : Equiv A) (i : nat), Proper (equiv ==> equiv) (delete i)
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A)
    +  → ∀ (f : A → A) (i : nat), Proper (equiv ==> equiv) f → Proper (equiv ==> equiv) (alter f i)
    +list_insert_proper:
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A) → ∀ i : nat, Proper (equiv ==> equiv ==> equiv) (insert i)
    +list_inserts_proper:
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A) → ∀ i : nat, Proper (equiv ==> equiv ==> equiv) (list_inserts i)
    +list_delete_proper:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ i : nat, Proper (equiv ==> equiv) (delete i)
     option_list_proper:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv) option_list
     list_filter_proper:
    -  ∀ (A : Type) (H : Equiv A) (P : A → Prop) (H0 : ∀ x : A, Decision (P x)),
    -  Proper (equiv ==> iff) P → Proper (equiv ==> equiv) (filter P)
    -replicate_proper: ∀ (A : Type) (H : Equiv A) (n : nat), Proper (equiv ==> equiv) (replicate n)
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A)
    +  → ∀ (P : A → Prop) (H0 : ∀ x : A, Decision (P x)),
    +    Proper (equiv ==> iff) P → Proper (equiv ==> equiv) (filter P)
    +replicate_proper:
    +  ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ n : nat, Proper (equiv ==> equiv) (replicate n)
     reverse_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv) reverse
     last_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv) last
     resize_proper:
    @@ -21963,19 +21985,28 @@
       Cofe B
       → Inhabited B → ∀ fB : A → B → B, (∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) → A → B
     fixpoint_AB_contractive:
    -  ∀ (A B : ofeT) (H0 : Cofe B) (Inhabited1 : Inhabited B) (fB : A → B → B)
    -  (H2 : ∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) (n : nat),
    -  Proper (dist_later n ==> dist n) (ofe.fixpoint_AB fB)
    +  ∀ A : ofeT,
    +  Cofe A
    +  → ∀ (B : ofeT) (H0 : Cofe B),
    +    Inhabited A
    +    → ∀ (Inhabited1 : Inhabited B) (fA : A → B → A) (fB : A → B → B),
    +      (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    +      → ∀ (H2 : ∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) (n : nat),
    +        Proper (dist_later n ==> dist n) (ofe.fixpoint_AB fB)
     ofe.fixpoint_AA:
       ∀ A B : ofeT,
       Cofe B
       → Inhabited B
         → (A → B → A) → ∀ fB : A → B → B, (∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) → A → A
     fixpoint_AA_contractive:
    -  ∀ (A B : ofeT) (H0 : Cofe B) (Inhabited1 : Inhabited B) (fA : A → B → A) (fB : A → B → B),
    -  (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    -  → ∀ (H2 : ∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) (n : nat),
    -    Proper (dist_later n ==> dist n) (ofe.fixpoint_AA fA fB)
    +  ∀ A : ofeT,
    +  Cofe A
    +  → ∀ (B : ofeT) (H0 : Cofe B),
    +    Inhabited A
    +    → ∀ (Inhabited1 : Inhabited B) (fA : A → B → A) (fB : A → B → B),
    +      (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    +      → ∀ (H2 : ∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) (n : nat),
    +        Proper (dist_later n ==> dist n) (ofe.fixpoint_AA fA fB)
     fixpoint_A:
       ∀ A : ofeT,
       Cofe A
    @@ -22007,11 +22038,27 @@
       (H2 : ∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB),
       fB (fixpoint_A fA fB) (fixpoint_B fA fB) ≡ fixpoint_B fA fB
     Proper_instance_0:
    -  ∀ (A B : ofeT) (fA : A → B → A),
    -  (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA) → Proper (equiv ==> equiv ==> equiv) fA
    +  ∀ A : ofeT,
    +  Cofe A
    +  → ∀ B : ofeT,
    +    Cofe B
    +    → Inhabited A
    +      → Inhabited B
    +        → ∀ (fA : A → B → A) (fB : A → B → B),
    +          (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    +          → (∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB)
    +            → Proper (equiv ==> equiv ==> equiv) fA
     Proper_instance_1:
    -  ∀ (A B : ofeT) (fB : A → B → B),
    -  (∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB) → Proper (equiv ==> equiv ==> equiv) fB
    +  ∀ A : ofeT,
    +  Cofe A
    +  → ∀ B : ofeT,
    +    Cofe B
    +    → Inhabited A
    +      → Inhabited B
    +        → ∀ (fA : A → B → A) (fB : A → B → B),
    +          (∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    +          → (∀ n : nat, Proper (dist_later n ==> dist_later n ==> dist n) fB)
    +            → Proper (equiv ==> equiv ==> equiv) fB
     fixpoint_A_unique:
       ∀ (A : ofeT) (H : Cofe A) (B : ofeT) (H0 : Cofe B) (Inhabited0 : Inhabited A) (Inhabited1 : Inhabited B)
       (fA : A → B → A) (fB : A → B → B) (H1 : ∀ n : nat, Proper (dist_later n ==> dist n ==> dist n) fA)
    @@ -22656,27 +22703,35 @@
     option_Forall2_trans: ∀ (A : Type) (R : relation A), Transitive R → Transitive (option_Forall2 R)
     option_Forall2_equiv: ∀ (A : Type) (R : relation A), Equivalence R → Equivalence (option_Forall2 R)
     option_equiv: ∀ A : Type, Equiv A → Equiv (option A)
    -equiv_option_Forall2: ∀ (A : Type) (H : Equiv A) (mx my : option A), mx ≡ my ↔ option_Forall2 equiv mx my
    +equiv_option_Forall2:
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A) → ∀ mx my : option A, mx ≡ my ↔ option_Forall2 equiv mx my
     option_equivalence:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Equivalence (equiv : relation (option A))
    -Some_proper: ∀ (A : Type) (H : Equiv A), Proper (equiv ==> equiv) Some
    -Some_equiv_inj: ∀ (A : Type) (H : Equiv A), Inj equiv equiv Some
    +Some_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> equiv) Some
    +Some_equiv_inj: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Inj equiv equiv Some
     option_leibniz:
       ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → LeibnizEquiv A → LeibnizEquiv (option A)
     equiv_None: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → ∀ mx : option A, mx ≡ None ↔ mx = None
     equiv_Some_inv_l:
    -  ∀ (A : Type) (H : Equiv A) (mx my : option A) (x : A), mx ≡ my → mx = Some x → ∃ y : A, my = Some y ∧ x ≡ y
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A)
    +  → ∀ (mx my : option A) (x : A), mx ≡ my → mx = Some x → ∃ y : A, my = Some y ∧ x ≡ y
     equiv_Some_inv_r:
    -  ∀ (A : Type) (H : Equiv A) (mx my : option A) (y : A), mx ≡ my → my = Some y → ∃ x : A, mx = Some x ∧ x ≡ y
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A)
    +  → ∀ (mx my : option A) (y : A), mx ≡ my → my = Some y → ∃ x : A, mx = Some x ∧ x ≡ y
     equiv_Some_inv_l':
    -  ∀ (A : Type) (H : Equiv A) (my : option A) (x : A), Some x ≡ my → ∃ x' : A, Some x' = my ∧ x ≡ x'
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A) → ∀ (my : option A) (x : A), Some x ≡ my → ∃ x' : A, Some x' = my ∧ x ≡ x'
     equiv_Some_inv_r':
       ∀ (A : Type) (H : Equiv A),
       Equivalence (equiv : relation A) → ∀ (mx : option A) (y : A), mx ≡ Some y → ∃ y' : A, mx = Some y' ∧ y ≡ y'
    -is_Some_proper: ∀ (A : Type) (H : Equiv A), Proper (equiv ==> iff) is_Some
    +is_Some_proper: ∀ (A : Type) (H : Equiv A), Equivalence (equiv : relation A) → Proper (equiv ==> iff) is_Some
     from_option_proper:
    -  ∀ (A : Type) (H : Equiv A) (B : Type) (R : relation B) (f : A → B),
    -  Proper (equiv ==> R) f → Proper (R ==> equiv ==> R) (from_option f)
    +  ∀ (A : Type) (H : Equiv A),
    +  Equivalence (equiv : relation A)
    +  → ∀ (B : Type) (R : relation B) (f : A → B), Proper (equiv ==> R) f → Proper (R ==> equiv ==> R) (from_option f)
     option_eq_None_dec: ∀ (A : Type) (mx : option A), Decision (mx = None)
     option_None_eq_dec: ∀ (A : Type) (mx : option A), Decision (None = mx)
     option_eq_dec: ∀ A : Type, EqDecision A → EqDecision (option A)
    @@ -23578,16 +23633,22 @@
     sts_ctx:
       ∀ Σ : gFunctors, invG Σ → ∀ sts : stsT, stsG Σ sts → gname → namespace → (sts.state sts → iProp Σ) → iProp Σ
     sts_inv_ne:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (n : nat),
    -  Proper (pointwise_relation (sts.state sts) (dist n) ==> dist n) (sts_inv γ)
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (n : nat),
    +    Proper (pointwise_relation (sts.state sts) (dist n) ==> dist n) (sts_inv γ)
     sts_inv_proper:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname),
    -  Proper (pointwise_relation (sts.state sts) equiv ==> equiv) (sts_inv γ)
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname),
    +    Proper (pointwise_relation (sts.state sts) equiv ==> equiv) (sts_inv γ)
     sts_ownS_proper:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname), Proper (equiv ==> equiv ==> equiv) (sts_ownS γ)
    +  ∀ Σ : gFunctors,
    +  invG Σ → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname), Proper (equiv ==> equiv ==> equiv) (sts_ownS γ)
     sts_own_proper:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (s : sts.state sts),
    -  Proper (equiv ==> equiv) (sts_own γ s)
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (s : sts.state sts), Proper (equiv ==> equiv) (sts_own γ s)
     sts_ctx_ne:
       ∀ (Σ : gFunctors) (H : invG Σ) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (n : nat) 
       (N : namespace), Proper (pointwise_relation (sts.state sts) (dist n) ==> dist n) (sts_ctx γ N)
    @@ -23598,24 +23659,38 @@
       ∀ (Σ : gFunctors) (H : invG Σ) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (N : namespace)
       (φ : sts.state sts → iProp Σ), PersistentP (sts_ctx γ N φ)
     sts_own_peristent:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (s : sts.state sts), PersistentP (sts_own γ s ∅)
    +  ∀ Σ : gFunctors,
    +  invG Σ → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (s : sts.state sts), PersistentP (sts_own γ s ∅)
     sts_ownS_peristent:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (S : sts.states sts), PersistentP (sts_ownS γ S ∅)
    +  ∀ Σ : gFunctors,
    +  invG Σ → ∀ (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (S : sts.states sts), PersistentP (sts_ownS γ S ∅)
     Params_instance_0: Params (@sts_inv) 4
     Params_instance_1: Params (@sts_ownS) 4
     Params_instance_2: Params (@sts_own) 5
     Params_instance_3: Params (@sts_ctx) 6
     sts_ownS_weaken:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (S1 S2 : sts.states sts) 
    -  (T1 T2 : sts.tokens sts), T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 → sts_ownS γ S1 T1 -∗ |==> sts_ownS γ S2 T2
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts),
    +    (sts.state sts → iProp Σ)
    +    → ∀ (γ : gname) (S1 S2 : sts.states sts) (T1 T2 : sts.tokens sts),
    +      T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 → sts_ownS γ S1 T1 -∗ |==> sts_ownS γ S2 T2
     sts_own_weaken:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (s : sts.state sts) (S : sts.states sts)
    -  (T1 T2 : sts.tokens sts), T2 ⊆ T1 → s ∈ S → sts.closed S T2 → sts_own γ s T1 -∗ |==> sts_ownS γ S T2
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts),
    +    (sts.state sts → iProp Σ)
    +    → ∀ (γ : gname) (s : sts.state sts) (S : sts.states sts) (T1 T2 : sts.tokens sts),
    +      T2 ⊆ T1 → s ∈ S → sts.closed S T2 → sts_own γ s T1 -∗ |==> sts_ownS γ S T2
     sts_ownS_op:
    -  ∀ (Σ : gFunctors) (sts : stsT) (H0 : stsG Σ sts) (γ : gname) (S1 S2 : sts.states sts) 
    -  (T1 T2 : sts.tokens sts),
    -  T1 ⊥ T2
    -  → sts.closed S1 T1 → sts.closed S2 T2 → sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ∗ sts_ownS γ S2 T2)%I
    +  ∀ Σ : gFunctors,
    +  invG Σ
    +  → ∀ (sts : stsT) (H0 : stsG Σ sts),
    +    (sts.state sts → iProp Σ)
    +    → ∀ (γ : gname) (S1 S2 : sts.states sts) (T1 T2 : sts.tokens sts),
    +      T1 ⊥ T2
    +      → sts.closed S1 T1
    +        → sts.closed S2 T2 → sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ∗ sts_ownS γ S2 T2)%I
     sts_alloc:
       ∀ (Σ : gFunctors) (H : invG Σ) (sts : stsT) (H0 : stsG Σ sts) (φ : sts.state sts → iProp Σ) 
       (E : coPset) (N : namespace) (s : sts.state sts),
    @@ -23708,7 +23783,8 @@
       CMRATotal A
       → CMRADiscrete A → ∀ (x : A) (P : A → Prop), x ~~>: P ↔ (∀ z : A, ✓ (x ⋅ z) → ∃ y : A, P y ∧ ✓ (y ⋅ z))
     cmra_discrete_update:
    -  ∀ A : cmraT, CMRATotal A → CMRADiscrete A → ∀ x y : A, x ~~> y ↔ (∀ z : A, ✓ (x ⋅ z) → ✓ (y ⋅ z))
    +  ∀ A : cmraT,
    +  CMRATotal A → CMRADiscrete A → CMRADiscrete A → ∀ x y : A, x ~~> y ↔ (∀ z : A, ✓ (x ⋅ z) → ✓ (y ⋅ z))
     cmra_transport_updateP:
       ∀ (A B : cmraT) (H : A = B) (P : A → Prop) (Q : B → Prop) (x : A),
       x ~~>: P → (∀ y : A, P y → Q (cmra_transport H y)) → cmra_transport H x ~~>: Q
    @@ -24042,8 +24118,7 @@
     wsat.ownD: ∀ Σ : gFunctors, invG Σ → gset positive → iProp Σ
     wsat.Params_instance_2: Params (@wsat.ownD) 3
     wsat.wsat: ∀ Σ : gFunctors, invG Σ → iProp Σ
    -wsat.invariant_unfold_contractive:
    -  ∀ (Σ : gFunctors) (n : nat), Proper (dist_later n ==> dist n) wsat.invariant_unfold
    +wsat.invariant_unfold_contractive: ∀ Σ : gFunctors, invG Σ → Contractive wsat.invariant_unfold
     wsat.ownI_contractive:
       ∀ (Σ : gFunctors) (H : invG Σ) (i : positive) (n : nat), Proper (dist_later n ==> dist n) (wsat.ownI i)
     wsat.ownI_persistent: ∀ (Σ : gFunctors) (H : invG Σ) (i : positive) (P : iProp Σ), PersistentP (wsat.ownI i P)
    @@ -32691,7 +32766,9 @@
     sel_patterns.sel_pat.parse: string → list sel_patterns.sel_pat
     cofe_solver.solver.A: cFunctor → nat → ofeT
     cofe_solver.solver.Cofe_instance_0:
    -  ∀ F : cFunctor, (∀ T : ofeT, Cofe T → Cofe (F T)) → ∀ k : nat, Cofe (cofe_solver.solver.A F k)
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T)) → Inhabited (F unitC) → ∀ k : nat, Cofe (cofe_solver.solver.A F k)
     cofe_solver.solver.f:
       ∀ F : cFunctor, Inhabited (F unitC) → ∀ k : nat, cofe_solver.solver.A F k -n> cofe_solver.solver.A F (S k)
     cofe_solver.solver.g:
    @@ -32705,13 +32782,15 @@
     cofe_solver.solver.gf:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F k),
    -    (cofe_solver.solver.g F k) ((cofe_solver.solver.f F k) x) ≡ x
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.g F k) ((cofe_solver.solver.f F k) x) ≡ x
     cofe_solver.solver.fg:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F (S (S k))),
    -    (cofe_solver.solver.f F (S k)) ((cofe_solver.solver.g F (S k)) x) ≡{k}≡ x
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F (S (S k))),
    +      (cofe_solver.solver.f F (S k)) ((cofe_solver.solver.g F (S k)) x) ≡{k}≡ x
     cofe_solver.solver.tower: ∀ F : cFunctor, Inhabited (F unitC) → Type
     cofe_solver.solver.Build_tower:
       ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (tower_car : ∀ k : nat, cofe_solver.solver.A F k),
    @@ -32724,17 +32803,21 @@
     cofe_solver.solver.tower_equiv: ∀ (F : cFunctor) (Finh : Inhabited (F unitC)), Equiv (cofe_solver.solver.tower F)
     cofe_solver.solver.tower_dist: ∀ (F : cFunctor) (Finh : Inhabited (F unitC)), Dist (cofe_solver.solver.tower F)
     cofe_solver.solver.tower_ofe_mixin:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)), OfeMixin (cofe_solver.solver.tower F)
    -cofe_solver.solver.T: ∀ F : cFunctor, Inhabited (F unitC) → ofeT
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T)) → ∀ Finh : Inhabited (F unitC), OfeMixin (cofe_solver.solver.tower F)
    +cofe_solver.solver.T:
    +  ∀ F : cFunctor, cFunctorContractive F → (∀ T : ofeT, Cofe T → Cofe (F T)) → Inhabited (F unitC) → ofeT
     cofe_solver.solver.tower_chain_obligation_1:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (c : chain (cofe_solver.solver.T F)) (k n i : nat),
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (c : chain (cofe_solver.solver.T F)) (k n i : nat),
       (n ≤ i)%nat → (c i) k ≡{n}≡ (c n) k
     cofe_solver.solver.tower_chain:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)),
    -  chain (cofe_solver.solver.T F) → ∀ k : nat, chain (cofe_solver.solver.A F k)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), chain (cofe_solver.solver.T F) → ∀ k : nat, chain (cofe_solver.solver.A F k)
     cofe_solver.solver.tower_compl_obligation_1:
    -  ∀ (F : cFunctor) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T)) (Finh : Inhabited (F unitC))
    -  (c : chain (cofe_solver.solver.T F)) (k : nat)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (c : chain (cofe_solver.solver.T F)) (k : nat)
       (H:=
        (λ x y : cofe_solver.solver.A F k, match equiv_dist x y with
                                           | conj _ x1 => x1
    @@ -32743,15 +32826,15 @@
       (cofe_solver.solver.g F k) (compl (cofe_solver.solver.tower_chain F c (S k)))
       ≡ compl (cofe_solver.solver.tower_chain F c k)
     cofe_solver.solver.tower_compl:
    -  ∀ F : cFunctor,
    -  (∀ T : ofeT, Cofe T → Cofe (F T))
    -  → ∀ Finh : Inhabited (F unitC), chain (cofe_solver.solver.T F) → cofe_solver.solver.T F
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), chain (cofe_solver.solver.T F) → cofe_solver.solver.T F
     cofe_solver.solver.tower_cofe_obligation_1:
    -  ∀ (F : cFunctor) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T)) (Finh : Inhabited (F unitC)) 
    -  (n : nat) (c : chain (cofe_solver.solver.T F)), cofe_solver.solver.tower_compl F c ≡{n}≡ 
    -  c n
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (n : nat) (c : chain (cofe_solver.solver.T F)),
    +  cofe_solver.solver.tower_compl F c ≡{n}≡ c n
     cofe_solver.solver.tower_cofe:
    -  ∀ F : cFunctor, (∀ T : ofeT, Cofe T → Cofe (F T)) → ∀ Finh : Inhabited (F unitC), Cofe (cofe_solver.solver.T F)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), Cofe (cofe_solver.solver.T F)
     cofe_solver.solver.ff:
       ∀ F : cFunctor, Inhabited (F unitC) → ∀ k i : nat, cofe_solver.solver.A F k -n> cofe_solver.solver.A F (i + k)
     cofe_solver.solver.gg:
    @@ -32759,89 +32842,120 @@
     cofe_solver.solver.ggff:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (x : cofe_solver.solver.A F k),
    -    (cofe_solver.solver.gg F i) ((cofe_solver.solver.ff F i) x) ≡ x
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.gg F i) ((cofe_solver.solver.ff F i) x) ≡ x
     cofe_solver.solver.f_tower:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat) (X : cofe_solver.solver.tower F),
    -    (cofe_solver.solver.f F (S k)) (X (S k)) ≡{k}≡ X (S (S k))
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k : nat) (X : cofe_solver.solver.tower F),
    +      (cofe_solver.solver.f F (S k)) (X (S k)) ≡{k}≡ X (S (S k))
     cofe_solver.solver.ff_tower:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (X : cofe_solver.solver.tower F),
    -    (cofe_solver.solver.ff F i) (X (S k)) ≡{k}≡ X (i + S k)%nat
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (X : cofe_solver.solver.tower F),
    +      (cofe_solver.solver.ff F i) (X (S k)) ≡{k}≡ X (i + S k)%nat
     cofe_solver.solver.gg_tower:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k i : nat) (X : cofe_solver.solver.tower F),
    -  (cofe_solver.solver.gg F i) (X (i + k)%nat) ≡ X k
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (X : cofe_solver.solver.tower F),
    +      (cofe_solver.solver.gg F i) (X (i + k)%nat) ≡ X k
     cofe_solver.solver.tower_car_ne:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (n k : nat),
    -  Proper (dist n ==> dist n) (λ X : cofe_solver.solver.tower F, X k)
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (n k : nat),
    +      Proper (dist n ==> dist n) (λ X : cofe_solver.solver.tower F, X k)
     cofe_solver.solver.project:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.T F -n> cofe_solver.solver.A F k
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.T F -n> cofe_solver.solver.A F k
     cofe_solver.solver.coerce:
       ∀ (F : cFunctor) (i j : nat), i = j → cofe_solver.solver.A F i -n> cofe_solver.solver.A F j
     cofe_solver.solver.coerce_id:
    -  ∀ (F : cFunctor) (i : nat) (H : i = i) (x : cofe_solver.solver.A F i), (cofe_solver.solver.coerce F H) x = x
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → Inhabited (F unitC)
    +      → ∀ (i : nat) (H : i = i) (x : cofe_solver.solver.A F i), (cofe_solver.solver.coerce F H) x = x
     cofe_solver.solver.coerce_proper:
    -  ∀ (F : cFunctor) (i j : nat) (x y : cofe_solver.solver.A F i) (H1 H2 : i = j),
    -  x = y → (cofe_solver.solver.coerce F H1) x = (cofe_solver.solver.coerce F H2) y
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → Inhabited (F unitC)
    +      → ∀ (i j : nat) (x y : cofe_solver.solver.A F i) (H1 H2 : i = j),
    +        x = y → (cofe_solver.solver.coerce F H1) x = (cofe_solver.solver.coerce F H2) y
     cofe_solver.solver.g_coerce:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k j : nat) (H : S k = S j) (x : cofe_solver.solver.A F (S k)),
    -  (cofe_solver.solver.g F j) ((cofe_solver.solver.coerce F H) x) =
    -  (cofe_solver.solver.coerce F (Nat.succ_inj k j H)) ((cofe_solver.solver.g F k) x)
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k j : nat) (H : S k = S j) (x : cofe_solver.solver.A F (S k)),
    +      (cofe_solver.solver.g F j) ((cofe_solver.solver.coerce F H) x) =
    +      (cofe_solver.solver.coerce F (Nat.succ_inj k j H)) ((cofe_solver.solver.g F k) x)
     cofe_solver.solver.coerce_f:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k j : nat) (H : S k = S j) (x : cofe_solver.solver.A F k),
    -  (cofe_solver.solver.coerce F H) ((cofe_solver.solver.f F k) x) =
    -  (cofe_solver.solver.f F j) ((cofe_solver.solver.coerce F (Nat.succ_inj k j H)) x)
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k j : nat) (H : S k = S j) (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.coerce F H) ((cofe_solver.solver.f F k) x) =
    +      (cofe_solver.solver.f F j) ((cofe_solver.solver.coerce F (Nat.succ_inj k j H)) x)
     cofe_solver.solver.gg_gg:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k i i1 i2 j : nat) (H1 : k = (i + j)%nat)
    -  (H2 : k = (i2 + (i1 + j))%nat) (x : cofe_solver.solver.A F k),
    -  (cofe_solver.solver.gg F i) ((cofe_solver.solver.coerce F H1) x) =
    -  (cofe_solver.solver.gg F i1) ((cofe_solver.solver.gg F i2) ((cofe_solver.solver.coerce F H2) x))
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i i1 i2 j : nat) (H1 : k = (i + j)%nat) (H2 : k = (i2 + (i1 + j))%nat)
    +      (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.gg F i) ((cofe_solver.solver.coerce F H1) x) =
    +      (cofe_solver.solver.gg F i1) ((cofe_solver.solver.gg F i2) ((cofe_solver.solver.coerce F H2) x))
     cofe_solver.solver.ff_ff:
    -  ∀ (F : cFunctor) (Finh : Inhabited (F unitC)) (k i i1 i2 j : nat) (H1 : (i + k)%nat = j)
    -  (H2 : (i1 + (i2 + k))%nat = j) (x : cofe_solver.solver.A F k),
    -  (cofe_solver.solver.coerce F H1) ((cofe_solver.solver.ff F i) x) =
    -  (cofe_solver.solver.coerce F H2) ((cofe_solver.solver.ff F i1) ((cofe_solver.solver.ff F i2) x))
    +  ∀ F : cFunctor,
    +  cFunctorContractive F
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i i1 i2 j : nat) (H1 : (i + k)%nat = j) (H2 : (i1 + (i2 + k))%nat = j)
    +      (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.coerce F H1) ((cofe_solver.solver.ff F i) x) =
    +      (cofe_solver.solver.coerce F H2) ((cofe_solver.solver.ff F i1) ((cofe_solver.solver.ff F i2) x))
     cofe_solver.solver.embed_coerce:
       ∀ F : cFunctor, Inhabited (F unitC) → ∀ k i : nat, cofe_solver.solver.A F k -n> cofe_solver.solver.A F i
     cofe_solver.solver.g_embed_coerce:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (x : cofe_solver.solver.A F k),
    -    (cofe_solver.solver.g F i) ((cofe_solver.solver.embed_coerce F (S i)) x)
    -    ≡ (cofe_solver.solver.embed_coerce F i) x
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k i : nat) (x : cofe_solver.solver.A F k),
    +      (cofe_solver.solver.g F i) ((cofe_solver.solver.embed_coerce F (S i)) x)
    +      ≡ (cofe_solver.solver.embed_coerce F i) x
     cofe_solver.solver.embed_obligation_1:
       ∀ F : cFunctor,
       cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F k) (i : nat),
    -    (cofe_solver.solver.g F i) ((cofe_solver.solver.embed_coerce F (S i)) x)
    -    ≡ (cofe_solver.solver.embed_coerce F i) x
    +  → (∀ T : ofeT, Cofe T → Cofe (F T))
    +    → ∀ (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F k) (i : nat),
    +      (cofe_solver.solver.g F i) ((cofe_solver.solver.embed_coerce F (S i)) x)
    +      ≡ (cofe_solver.solver.embed_coerce F i) x
     cofe_solver.solver.embed:
    -  ∀ F : cFunctor,
    -  cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.A F k → cofe_solver.solver.T F
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.A F k → cofe_solver.solver.T F
     cofe_solver.solver.Params_instance_0:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)),
    -  Params (cofe_solver.solver.embed F) 1
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), Params (cofe_solver.solver.embed F) 1
     cofe_solver.solver.embed_ne:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (k n : nat),
    -  Proper (dist n ==> dist n) (cofe_solver.solver.embed F k)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k n : nat), Proper (dist n ==> dist n) (cofe_solver.solver.embed F k)
     cofe_solver.solver.embed':
    -  ∀ F : cFunctor,
    -  cFunctorContractive F
    -  → ∀ (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.A F k -n> cofe_solver.solver.T F
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k : nat), cofe_solver.solver.A F k -n> cofe_solver.solver.T F
     cofe_solver.solver.embed_f:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (k : nat)
    -  (x : cofe_solver.solver.A F k),
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k : nat) (x : cofe_solver.solver.A F k),
       cofe_solver.solver.embed F (S k) ((cofe_solver.solver.f F k) x) ≡ cofe_solver.solver.embed F k x
     cofe_solver.solver.embed_tower:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (k : nat)
    -  (X : cofe_solver.solver.T F), cofe_solver.solver.embed F (S k) (X (S k)) ≡{k}≡ X
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (k : nat) (X : cofe_solver.solver.T F),
    +  cofe_solver.solver.embed F (S k) (X (S k)) ≡{k}≡ X
     cofe_solver.solver.unfold_chain_obligation_1:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (X : cofe_solver.solver.T F)
    -  (n i : nat) (Hi : (n ≤ i)%nat)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (X : cofe_solver.solver.T F) (n i : nat) (Hi : (n ≤ i)%nat)
       (H:=
        ex_intro (λ k : nat, i = (k + n)%nat) (i - n)%nat
          (Nat2Z.inj i (i - n + n)
    @@ -32931,31 +33045,28 @@
       (cFunctor_map F (cofe_solver.solver.project F i, cofe_solver.solver.embed' F i)) (X (S i)) ≡{n}≡ 
       (cFunctor_map F (cofe_solver.solver.project F n, cofe_solver.solver.embed' F n)) (X (S n))
     cofe_solver.solver.unfold_chain:
    -  ∀ F : cFunctor,
    -  cFunctorContractive F
    -  → ∀ Finh : Inhabited (F unitC), cofe_solver.solver.T F → chain (F (cofe_solver.solver.T F))
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), cofe_solver.solver.T F → chain (F (cofe_solver.solver.T F))
     cofe_solver.solver.unfold:
    -  ∀ F : cFunctor,
    -  cFunctorContractive F
    -  → (∀ T : ofeT, Cofe T → Cofe (F T))
    -    → ∀ Finh : Inhabited (F unitC), cofe_solver.solver.T F → F (cofe_solver.solver.T F)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), cofe_solver.solver.T F → F (cofe_solver.solver.T F)
     cofe_solver.solver.unfold_ne:
       ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
       (Finh : Inhabited (F unitC)) (n : nat), Proper (dist n ==> dist n) (cofe_solver.solver.unfold F)
     cofe_solver.solver.fold_obligation_1:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (X : F (cofe_solver.solver.T F))
    -  (k : nat),
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (X : F (cofe_solver.solver.T F)) (k : nat),
       (cofe_solver.solver.g F k)
         ((cofe_solver.solver.g F (S k))
            ((cFunctor_map F (cofe_solver.solver.embed' F (S k), cofe_solver.solver.project F (S k))) X))
       ≡ (cofe_solver.solver.g F k)
           ((cFunctor_map F (cofe_solver.solver.embed' F k, cofe_solver.solver.project F k)) X)
     cofe_solver.solver.fold:
    -  ∀ F : cFunctor,
    -  cFunctorContractive F → ∀ Finh : Inhabited (F unitC), F (cofe_solver.solver.T F) → cofe_solver.solver.T F
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)), F (cofe_solver.solver.T F) → cofe_solver.solver.T F
     cofe_solver.solver.fold_ne:
    -  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Finh : Inhabited (F unitC)) (n : nat),
    -  Proper (dist n ==> dist n) (cofe_solver.solver.fold F)
    +  ∀ (F : cFunctor) (Fcontr : cFunctorContractive F) (Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T))
    +  (Finh : Inhabited (F unitC)) (n : nat), Proper (dist n ==> dist n) (cofe_solver.solver.fold F)
     cofe_solver.solver.result:
       ∀ F : cFunctor,
       cFunctorContractive F → (∀ T : ofeT, Cofe T → Cofe (F T)) → Inhabited (F unitC) → cofe_solver.solution F
    @@ -33694,15 +33805,17 @@
       (Φ : val → uPred (iResUR Σ)),
       True -∗ ▷ (∀ l : loc, recv N l P ∗ send N l P -∗ Φ #l) -∗ WP newbarrier #() {{ v, Φ v }}
     ress_split:
    -  ∀ (Σ : gFunctors) (barrierG0 : barrierG Σ) (i i1 i2 : gname) (Q R1 R2 : ∙%CF (iProp Σ)) 
    -  (P : iProp Σ) (I : gset gname),
    -  i ∈ I
    -  → i1 ∉ I
    -    → i2 ∉ I
    -      → i1 ≠ i2
    -        → saved_prop_own i Q -∗
    -          saved_prop_own i1 R1 -∗
    -          saved_prop_own i2 R2 -∗ (Q -∗ R1 ∗ R2) -∗ ress P I -∗ ress P ({[i1; i2]} ∪ I ∖ {[i]})
    +  ∀ Σ : gFunctors,
    +  heapG Σ
    +  → ∀ (barrierG0 : barrierG Σ) (i i1 i2 : gname) (Q R1 R2 : ∙%CF (iProp Σ)) (P : iProp Σ) 
    +    (I : gset gname),
    +    i ∈ I
    +    → i1 ∉ I
    +      → i2 ∉ I
    +        → i1 ≠ i2
    +          → saved_prop_own i Q -∗
    +            saved_prop_own i1 R1 -∗
    +            saved_prop_own i2 R2 -∗ (Q -∗ R1 ∗ R2) -∗ ress P I -∗ ress P ({[i1; i2]} ∪ I ∖ {[i]})
     recv_ne:
       ∀ (Σ : gFunctors) (heapG0 : heapG Σ) (barrierG0 : barrierG Σ) (N : namespace) (n : nat) 
       (l : loc), Proper (dist n ==> dist n) (recv N l)
    @@ -33715,8 +33828,9 @@
     barrier_inv_ne:
       ∀ (Σ : gFunctors) (heapG0 : heapG Σ) (barrierG0 : barrierG Σ) (n : nat) (l : loc),
       Proper (dist n ==> eq ==> dist n) (barrier_inv l)
    -state_to_prop_ne: ∀ (Σ : gFunctors) (n : nat) (s : state), Proper (dist n ==> dist n) (state_to_prop s)
    -ress_ne: ∀ (Σ : gFunctors) (barrierG0 : barrierG Σ) (n : nat), Proper (dist n ==> eq ==> dist n) ress
    +state_to_prop_ne:
    +  ∀ Σ : gFunctors, heapG Σ → barrierG Σ → ∀ (n : nat) (s : state), Proper (dist n ==> dist n) (state_to_prop s)
    +ress_ne: ∀ Σ : gFunctors, heapG Σ → ∀ (barrierG0 : barrierG Σ) (n : nat), Proper (dist n ==> eq ==> dist n) ress
     barrier_ctx_persistent:
       ∀ (Σ : gFunctors) (heapG0 : heapG Σ) (barrierG0 : barrierG Σ) (N : namespace) (γ : gname) 
       (l : loc) (P : iProp Σ), PersistentP (barrier_ctx N γ l P)
    Edited by Ralf Jung
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment