Another bot -> invalid rename

diaframe/lib/own/proofmode_instances.v

@@ -383,7 +383,7 @@ Section recursive.
     by iRewrite "Ha".
   Qed.
   Global Instance sum_inl_inr_invalid_op {A B : cmra} (a : A) (b : B) Σ :
-    IsValidOp (CsumBot) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
+    IsValidOp (CsumInvalid) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
   Proof. 
     split; rewrite /op /= /cmra_op //=; eauto. (* TODO: need proper access to unsealing lemma's *)
     uPred_primitive.unseal.
@@ -391,7 +391,7 @@ Section recursive.
     rewrite /validN /= /cmra_validN //=.
   Qed.
   Global Instance sum_inr_inl_invalid_op {A B : cmra} (a : A) (b : B) Σ :
-    IsValidOp (CsumBot) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
+    IsValidOp (CsumInvalid) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
   Proof. 
     split; rewrite /op /= /cmra_op //=; eauto.
     uPred_primitive.unseal.
@@ -660,7 +660,7 @@ Section recursive.
   Qed.
 
   Global Instance excl_valid_op {O : ofe} (a1 a2 : excl O) Σ:
-    IsValidOp ExclBot a1 a2 Σ False%I.
+    IsValidOp ExclInvalid a1 a2 Σ False%I.
   Proof. split; rewrite excl_validI /=; eauto. Qed.
   Global Instance excl_included_merge {O : ofe} (o1 o2 : excl O) {Σ} :
     IsIncludedMerge o1 o2 (Σ := Σ) False%I.
@@ -1029,4 +1029,4 @@ Section recursive.
       iSplit => //.
   Qed.
 
-End recursive.
+End recursive.
\ No newline at end of file