Sealing session type subtyping relation

Seal subtyping relation for session types, to avoid breaking abstraction when applying subtyping rules and tactics

theories/logrel/subtyping.v

@@ -6,10 +6,17 @@ equivalent to having both [A <: B] and [B <: A]. Finally, the notion of a
 when [A <: copy A]. *)
 From actris.logrel Require Export model term_types.
 
+Definition lsty_le_def {Σ} (P1 P2 : lsty Σ) :=
+  iProto_le (lsty_car P1) (lsty_car P2).
+Definition lsty_le_aux : seal (@lsty_le_def). by eexists. Qed.
+Definition lsty_le := lsty_le_aux.(unseal).
+Definition lsty_le_eq : @lsty_le = @lsty_le_def := lsty_le_aux.(seal_eq).
+Arguments lsty_le {_} _ _.
+
 Definition lty_le {Σ k} : lty Σ k → lty Σ k → iProp Σ :=
   match k with
   | tty_kind => λ A1 A2, ■ ∀ v, ltty_car A1 v -∗ ltty_car A2 v
-  | lty_kind => λ P1 P2, ■ iProto_le (lsty_car P1) (lsty_car P2)
+  | lty_kind => λ P1 P2, ■ lsty_le P1 P2
   end%I.
 Arguments lty_le : simpl never.
 Infix "<:" := lty_le (at level 70) : bi_scope.
@@ -34,7 +41,9 @@ Section subtyping.
   Proof. rewrite /lty_bi_le /=. apply _. Qed.
 
   Global Instance lty_le_ne : NonExpansive2 (@lty_le Σ k).
-  Proof. destruct k; solve_proper. Qed.
+  Proof.
+    rewrite /lty_le lsty_le_eq. destruct k; rewrite ?/lsty_le_def; solve_proper.
+  Qed.
   Global Instance lty_le_proper {k} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ k).
   Proof. apply (ne_proper_2 _). Qed.
   Global Instance lty_bi_le_ne {k} : NonExpansive2 (@lty_bi_le Σ k).