diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index dbdb08b5f4d12e72cb3aa5811dab77003d682cd4..02c67710b9c889e6fc3f294cebaf3659dd30a147 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -107,6 +107,17 @@ Section sum.
         iDestruct "Hlen" as %<-. done.
   Qed.
 
+  Global Instance sum_proper E L:
+    Proper (Forall2 (eqtype E L) ==> eqtype E L) sum.
+  Proof.
+    (* TODO: Isn't there sth. showing that Forall2 is monotnous wrt. the predicate? *)
+    intros tyl1 tyl2 Heq.
+    assert (Forall2 (subtype E L) tyl1 tyl2 ∧ Forall2 (subtype E L) tyl2 tyl1).
+    { induction Heq as [|???? Heq]; first done. destruct_and!.
+      destruct Heq. split; constructor; done. }
+    destruct_and!. split; apply sum_mono; done.
+  Qed.
+
   (* TODO : Make the Forall parameter a typeclass *)
   (* TODO : This next step is suspuciously slow. *)
   Global Instance sum_copy tyl :