CMRAs with identity element are inhabited.

algebra/cmra.v

@@ -128,6 +128,7 @@ Class CMRAIdentity (A : cmraT) `{Empty A} : Prop := {
   cmra_empty_left_id :> LeftId (≡) ∅ (⋅);
   cmra_empty_timeless :> Timeless ∅
 }.
+Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate ∅.
 
 (** * Morphisms *)
 Class CMRAMonotone {A B : cmraT} (f : A → B) := {

program_logic/auth.v

@@ -16,10 +16,6 @@ Section auth.
   Hypothesis auth_valid :
     forall a b, (✓ (Auth (Excl a) b) : iProp Λ (globalC Σ)) ⊑ (∃ b', a ≡ b ⋅ b').
 
-  (* FIXME how much would break if we had a global instance from ∅ to Inhabited? *)
-  Local Instance auth_inhabited : Inhabited A.
-  Proof. split. exact ∅. Qed.
-
   Definition auth_inv (γ : gname) : iProp Λ (globalC Σ) :=
     (∃ a, own AuthI γ (● a) ★ φ a)%I.
   Definition auth_own (γ : gname) (a : A) : iProp Λ (globalC Σ) := own AuthI γ (◯ a).