Slightly clean up import for in-dec for Graph edges

Language/Graphs.agda

@@ -12,7 +12,6 @@ open import Data.List.Relation.Unary.Any as RelAny using ()
 open import Data.Nat as Nat using (ℕ; suc)
 open import Data.Nat.Properties using (+-assoc; +-comm)
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
-open import Data.Product.Properties as ProdProp using ()
 open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_)
 open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ; lookup-++ʳ)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)
@@ -122,7 +121,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
@@ -148,7 +147,11 @@ private
     finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))
 
 module _ (g : Graph) where
-    open import Data.List.Membership.DecPropositional (ProdProp.≡-dec (FinProp._≟_ {Graph.size g}) (FinProp._≟_ {Graph.size g})) using (_∈?_)
+    open import Data.Product.Properties as ProdProp using ()
+    private _≟_ = ProdProp.≡-dec (FinProp._≟_ {Graph.size g})
+                                 (FinProp._≟_ {Graph.size g})
+
+    open import Data.List.Membership.DecPropositional (_≟_) using (_∈?_)
 
     indices : List (Graph.Index g)
     indices = proj₁ (finValues (Graph.size g))

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⇒ρ₂))