Make uPred_si_embed instances lemmas and move them

iris/base_logic/upred.v

@@ -591,6 +591,20 @@ Proof.
   unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
 Qed.
 
+Lemma si_embed_mono :
+  Proper ((⊢@{siPropI}) ==> (⊢)) (@uPred_si_embed M).
+Proof. intros ?? Hm. unseal. split => ??? /=. by apply Hm. Qed.
+Lemma si_embed_ne :
+  NonExpansive (@uPred_si_embed M).
+Proof. intros ??? He. unseal. split => ???? /=. by apply He. Qed.
+Lemma si_embed_proper : Proper ((≡) ==> (≡)) (@uPred_si_embed M).
+Proof. apply ne_proper, si_embed_ne. Qed.
+
+Lemma si_emp_valid_ne : NonExpansive (@uPred_si_emp_valid M).
+Proof.
+  intros ??? He. unseal. split => ??. apply He; [done|apply ucmra_unit_validN].
+Qed.
+
 Lemma cmra_valid_ne {A : cmra} :
   NonExpansive (@uPred_cmra_valid M A).
 Proof.
@@ -890,18 +904,6 @@ Proof.
 Qed.
 
 (** Embedding of siProp *)
-Local Instance si_embed_mono :
-  Proper ((⊢@{siPropI}) ==> (⊢)) (@uPred_si_embed M).
-Proof. intros ?? Hm. unseal. split => ??? /=. by apply Hm. Qed.
-Local Instance si_embed_ne : NonExpansive (@uPred_si_embed M).
-Proof. intros ??? He. unseal. split => ???? /=. by apply He. Qed.
-Local Instance si_embed_proper : Proper ((≡) ==> (≡)) (@uPred_si_embed M).
-Proof. apply ne_proper, _. Qed.
-Local Instance si_emp_valid_ne : NonExpansive (@uPred_si_emp_valid M).
-Proof.
-  intros ??? He. unseal. split => ??. apply He; [done|apply ucmra_unit_validN].
-Qed.
-
 Local Notation "⎡ P ⎤" := (@uPred_si_embed M (P : siProp)) : bi_scope.
 Local Ltac unseal_embed :=
   rewrite /bi_emp /= /siProp_emp /= ?siProp_pure_eq /=