Add some helpers and rewrite code

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Language/Properties.agda

@@ -6,7 +6,7 @@ open import Language.Graphs
 open import Language.Traces
 
 open import Data.Fin as Fin using (zero)
-open import Data.List using (_∷_; [])
+open import Data.List using (List; _∷_; [])
 open import Data.List.Relation.Unary.Any using (here)
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
 open import Data.Product using (Σ; _,_; _×_)
@@ -104,15 +104,22 @@ _++_ {g₁} {g₂} etr₁ etr₂
                 (Trace-↦ʳ g₁ g₂ (EndToEndTrace.trace etr₂))
         }
 
+Trace-singleton : ∀ {bss : List BasicStmt} {ρ₁ ρ₂ : Env} →
+                  ρ₁ , bss ⇒ᵇˢ ρ₂ → EndToEndTrace {singleton bss} ρ₁ ρ₂
+Trace-singleton ρ₁⇒ρ₂ = record
+    { idx₁ = zero
+    ; idx₁∈inputs = here refl
+    ; idx₂ = zero
+    ; idx₂∈outputs = here refl
+    ; trace = Trace-single ρ₁⇒ρ₂
+    }
+
+Trace-singleton[] : ∀ (ρ : Env) → EndToEndTrace {singleton []} ρ ρ
+Trace-singleton[] env = Trace-singleton []
+
 buildCfg-sufficient : ∀ {s : Stmt} {ρ₁ ρ₂ : Env} → ρ₁ , s ⇒ˢ ρ₂ →
                       EndToEndTrace {buildCfg s} ρ₁ ρ₂
 buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) =
-    record
-        { idx₁ = zero
-        ; idx₁∈inputs = here refl
-        ; idx₂ = zero
-        ; idx₂∈outputs = here refl
-        ; trace = Trace-single (ρ₁,bs⇒ρ₂ ∷ [])
-        }
+    Trace-singleton (ρ₁,bs⇒ρ₂ ∷ [])
 buildCfg-sufficient (⇒ˢ-then ρ₁ ρ₂ ρ₃ s₁ s₂ ρ₁,s₁⇒ρ₂ ρ₂,s₂⇒ρ₃) =
     buildCfg-sufficient ρ₁,s₁⇒ρ₂ ++ buildCfg-sufficient ρ₂,s₂⇒ρ₃