Prove weakening for `typed`

Part of an answer to an Iris HelpDesk question — see https://mattermost.mpi-sws.org/iris/pl/m64hgftb8ffpmbdhnxkoo7ga8r.

theories/typing/types.v

@@ -349,3 +349,23 @@ Theorem typed_is_closed Γ e τ :
   Γ ⊢ₜ e : τ → is_closed_expr (dom Γ) e.
 Proof. intros. eapply is_closed_expr_set_sound, typed_is_closed_set; eauto. Qed.
 
+Lemma binder_insert_mono {V} (m1 m2 : stringmap V) (i : binder) (x : V) :
+  m1 ⊆ m2 → <[i:=x]> m1 ⊆ <[i:=x]> m2.
+Proof.
+  rewrite /insert/insert_binder /binder_insert/=.
+  case: i => [//|s]; apply insert_mono.
+Qed.
+
+#[local] Hint Constructors typed : core.
+(* [Hint Resolve] doesn't work for this hint. *)
+#[local] Hint Extern 10 (⤉ _ ⊆ ⤉ _) => simple apply map_fmap_mono : core.
+#[local] Hint Resolve lookup_weaken binder_insert_mono : core.
+
+Theorem typed_weaken Γ Γ' e τ :
+  Γ ⊢ₜ e : τ →
+  Γ ⊆ Γ' →
+  Γ' ⊢ₜ e : τ.
+Proof.
+  move: Γ' => + HT.
+  induction HT => Γ' HS; eauto 10.
+Qed.