diff --git a/Language/Properties.agda b/Language/Properties.agda
index 2fb870e..42fe80e 100644
--- a/Language/Properties.agda
+++ b/Language/Properties.agda
@@ -54,6 +54,35 @@ Trace-∙ʳ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
     Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ʳ _ (x∈xs⇒fx∈fxs (Graph.size g₁ ↑ʳ_) idx₁→idx))
                     (Trace-∙ʳ tr')
 
+EndToEndTrace-∙ˡ : ∀ {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env} →
+                   EndToEndTrace {g₁} ρ₁ ρ₂ →
+                   EndToEndTrace {g₁ ∙ g₂} ρ₁ ρ₂
+EndToEndTrace-∙ˡ {g₁} {g₂} etr = record
+    { idx₁ = EndToEndTrace.idx₁ etr Fin.↑ˡ Graph.size g₂
+    ; idx₁∈inputs = ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (Fin._↑ˡ Graph.size g₂)
+                                                    (EndToEndTrace.idx₁∈inputs etr))
+    ; idx₂ = EndToEndTrace.idx₂ etr Fin.↑ˡ Graph.size g₂
+    ; idx₂∈outputs = ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (Fin._↑ˡ Graph.size g₂)
+                                                    (EndToEndTrace.idx₂∈outputs etr))
+    ; trace = Trace-∙ˡ (EndToEndTrace.trace etr)
+    }
+
+EndToEndTrace-∙ʳ : ∀ {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env} →
+           EndToEndTrace {g₂} ρ₁ ρ₂ →
+           EndToEndTrace {g₁ ∙ g₂} ρ₁ ρ₂
+EndToEndTrace-∙ʳ {g₁} {g₂} etr = record
+    { idx₁ = Graph.size g₁ Fin.↑ʳ EndToEndTrace.idx₁ etr
+    ; idx₁∈inputs = ListMemProp.∈-++⁺ʳ (Graph.inputs g₁ ↑ˡⁱ Graph.size g₂)
+                                       ((x∈xs⇒fx∈fxs (Graph.size g₁ Fin.↑ʳ_)
+                                                     (EndToEndTrace.idx₁∈inputs etr)))
+    ; idx₂ = Graph.size g₁ Fin.↑ʳ EndToEndTrace.idx₂ etr
+    ; idx₂∈outputs = ListMemProp.∈-++⁺ʳ (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂)
+                                        ((x∈xs⇒fx∈fxs (Graph.size g₁ Fin.↑ʳ_)
+                                                      (EndToEndTrace.idx₂∈outputs etr)))
+
+    ; trace = Trace-∙ʳ (EndToEndTrace.trace etr)
+    }
+
 Trace-↦ˡ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} →
            Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ →
            Trace {g₁ ↦ g₂} (idx₁ Fin.↑ˡ Graph.size g₂) (idx₂ Fin.↑ˡ Graph.size g₂) ρ₁ ρ₂