diff --git a/Language/Graphs.agda b/Language/Graphs.agda
index e294eea..01d8e0a 100644
--- a/Language/Graphs.agda
+++ b/Language/Graphs.agda
@@ -122,7 +122,7 @@ wrap g = singleton [] ↦ g ↦ singleton []
 buildCfg : Stmt → Graph
 buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ [])
 buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
-buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton []
+buildCfg (if _ then s₁ else s₂) = buildCfg s₁ ∙ buildCfg s₂
 buildCfg (while _ repeat s) = loop (buildCfg s)
 
 private
diff --git a/Language/Properties.agda b/Language/Properties.agda
index b777adc..e9173fe 100644
--- a/Language/Properties.agda
+++ b/Language/Properties.agda
@@ -285,13 +285,9 @@ buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) =
 buildCfg-sufficient (⇒ˢ-then ρ₁ ρ₂ ρ₃ s₁ s₂ ρ₁,s₁⇒ρ₂ ρ₂,s₂⇒ρ₃) =
     buildCfg-sufficient ρ₁,s₁⇒ρ₂ ++ buildCfg-sufficient ρ₂,s₂⇒ρ₃
 buildCfg-sufficient (⇒ˢ-if-true ρ₁ ρ₂ _ _ s₁ s₂ _ _ ρ₁,s₁⇒ρ₂) =
-    EndToEndTrace-singleton[] ρ₁ ++
-    (EndToEndTrace-∙ˡ (buildCfg-sufficient ρ₁,s₁⇒ρ₂)) ++
-    EndToEndTrace-singleton[] ρ₂
+    EndToEndTrace-∙ˡ (buildCfg-sufficient ρ₁,s₁⇒ρ₂)
 buildCfg-sufficient (⇒ˢ-if-false ρ₁ ρ₂ _ s₁ s₂ _ ρ₁,s₂⇒ρ₂) =
-    EndToEndTrace-singleton[] ρ₁ ++
-    (EndToEndTrace-∙ʳ {buildCfg s₁} (buildCfg-sufficient ρ₁,s₂⇒ρ₂)) ++
-    EndToEndTrace-singleton[] ρ₂
+    EndToEndTrace-∙ʳ {buildCfg s₁} (buildCfg-sufficient ρ₁,s₂⇒ρ₂)
 buildCfg-sufficient (⇒ˢ-while-true ρ₁ ρ₂ ρ₃ _ _ s _ _ ρ₁,s⇒ρ₂ ρ₂,ws⇒ρ₃) =
     EndToEndTrace-loop² {buildCfg s}
                         (EndToEndTrace-loop {buildCfg s} (buildCfg-sufficient ρ₁,s⇒ρ₂))