diff --git a/FFOLInitial.agda b/FFOLInitial.agda
index 62632c3..cca3269 100644
--- a/FFOLInitial.agda
+++ b/FFOLInitial.agda
@@ -45,24 +45,35 @@ module FFOLInitial (F : Nat → Set) (R : Nat → Set) where
   zero [ σ ]tz = zero
   next t tz [ σ ]tz = next (t [ σ ]t) (tz [ σ ]tz)
 
+  -- tz application is like mapping
+  tzmap : {tz : Array (Tm Γₜ) n} {σ : Subt Δₜ Γₜ} → (tz [ σ ]tz) ≡ map (λ t → t [ σ ]t) tz
+  tzmap {tz = zero} = refl
+  tzmap {tz = next t tz} {σ = σ} = cong (next (t [ σ ]t)) tzmap
+
   -- We define liftings on term variables
   -- A term of n variables is a term of n+1 variables
-  liftt : Tm Γₜ → Tm (Γₜ ▹t⁰)
   -- Same for a term array
+  liftt : Tm Γₜ → Tm (Γₜ ▹t⁰)
   lifttz : Array (Tm Γₜ) n → Array (Tm (Γₜ ▹t⁰)) n
+  
   liftt (var tv) = var (tvnext tv)
   liftt (fun f tz) = fun f (lifttz tz)
   lifttz zero = zero
   lifttz (next t tz) = next (liftt t) (lifttz tz)
-  -- From a substitution into n variables, we construct a substitution from n+1 variables to n+1 variables which maps it to itself
-  -- i.e. 0 -> 0 and for all i ->(old) σ(i) we get i+1 -> σ(i)+1
-  lift : Subt Δₜ Γₜ → Subt (Δₜ ▹t⁰) (Γₜ ▹t⁰)
-  lift εₜ = wk▹t εₜ (var tvzero)
-  lift (wk▹t σ t) = wk▹t (lift σ) (liftt t)
+  
   -- From a substition into n variables, we get a substitution into n+1 variables which don't use the last one
   llift : Subt Δₜ Γₜ → Subt (Δₜ ▹t⁰) Γₜ
   llift εₜ = εₜ
   llift (wk▹t σ t) = wk▹t (llift σ) (liftt t)
+  llift-liftt : {tv : TmVar Γₜ} → {σ : Subt Δₜ Γₜ} → liftt (var tv [ σ ]t) ≡ var tv [ llift σ ]t
+  llift-liftt {tv = tvzero} {σ = wk▹t σ x} = refl
+  llift-liftt {tv = tvnext tv} {σ = wk▹t σ x} = llift-liftt {tv = tv} {σ = σ}
+  
+  -- From a substitution into n variables, we construct a substitution from n+1 variables to n+1 variables which maps it to itself
+  -- i.e. 0 -> 0 and for all i ->(old) σ(i) we get i+1 -> σ(i)+1
+  lift : Subt Δₜ Γₜ → Subt (Δₜ ▹t⁰) (Γₜ ▹t⁰)
+  lift σ = wk▹t (llift σ) (var tvzero)
+
   
   -- We subst on formulæ
   _[_]f : For Γₜ → Subt Δₜ Γₜ → For Δₜ
@@ -73,12 +84,13 @@ module FFOLInitial (F : Nat → Set) (R : Nat → Set) where
   -- We now can define identity on term substitutions       
   idₜ : Subt Γₜ Γₜ
   idₜ {◇t} = εₜ
-  idₜ {Γₜ ▹t⁰} = lift idₜ
+  idₜ {Γₜ ▹t⁰} = lift (idₜ {Γₜ})
 
   _∘ₜ_ : Subt Δₜ Γₜ → Subt Ξₜ Δₜ → Subt Ξₜ Γₜ
   εₜ ∘ₜ β = εₜ
   wk▹t α x ∘ₜ β = wk▹t (α ∘ₜ β) (x [ β ]t)
 
+
   -- We have the access functions from the algebra, in restricted versions
   πₜ¹ : Subt Δₜ (Γₜ ▹t⁰) → Subt Δₜ Γₜ
   πₜ¹ (wk▹t σₜ t) = σₜ
@@ -96,20 +108,46 @@ module FFOLInitial (F : Nat → Set) (R : Nat → Set) where
   ,ₜ∘πₜ {σₜ = wk▹t σₜ t} = refl
 
   -- We can also prove the substitution equalities
-  lem1 : lift (idₜ {Γₜ}) ≡ wk▹t {!!} {!!}
   []t-id : {t : Tm Γₜ} → t [ idₜ {Γₜ} ]t ≡ t
   []tz-id : {tz : Array (Tm Γₜ) n} → tz [ idₜ {Γₜ} ]tz ≡ tz
-  []t-id {◇t ▹t⁰} {var tvzero} = refl
-  []t-id {(Γₜ ▹t⁰) ▹t⁰} {var tv} = {!!}
+  []t-id {Γₜ ▹t⁰} {var tvzero} = refl
+  []t-id {Γₜ ▹t⁰} {var (tvnext tv)} = substP (λ t → t ≡ var (tvnext tv)) (llift-liftt {tv = tv} {σ = idₜ}) (substP (λ t → liftt t ≡ var (tvnext tv)) (≡sym ([]t-id {t = var tv})) refl)
   []t-id {Γₜ} {fun f tz} = substP (λ tz' → fun f tz' ≡ fun f tz) (≡sym []tz-id) refl
   []tz-id {tz = zero} = refl
   []tz-id {tz = next x tz} = substP (λ tz' → (next (x [ idₜ ]t) tz') ≡ next x tz) (≡sym []tz-id) (substP (λ x' → next x' tz ≡ next x tz) (≡sym []t-id) refl)
   []t-∘ : {α : Subt Ξₜ Δₜ} → {β : Subt Δₜ Γₜ} → {t : Tm Γₜ} → t [ β ∘ₜ α ]t ≡ (t [ β ]t) [ α ]t
-  []t-∘ {α = α} {β = β} {t = t} = {!!}
+  []tz-∘ : {α : Subt Ξₜ Δₜ} → {β : Subt Δₜ Γₜ} → {tz : Array (Tm Γₜ) n} → tz [ β ∘ₜ α ]tz ≡ (tz [ β ]tz) [ α ]tz
+  []tz-∘ {tz = zero} = refl
+  []tz-∘ {tz = next t tz} = cong₂ next ([]t-∘ {t = t}) []tz-∘
+  []t-∘ {α = α} {β = wk▹t β t} {t = var tvzero} = refl
+  []t-∘ {α = α} {β = wk▹t β t} {t = var (tvnext tv)} = []t-∘ {t = var tv}
+  []t-∘ {α = α} {β = β} {t = fun f tz} = cong (fun f) ([]tz-∘ {tz = tz})
   fun[] : {σ : Subt Δₜ Γₜ} → {f : F n} → {tz : Array (Tm Γₜ) n} → (fun f tz) [ σ ]t ≡ fun f (map (λ t → t [ σ ]t) tz)
+  fun[] {tz = zero} = refl
+  fun[] {σ = σ} {f = f} {tz = next t tz} = cong (fun f) (cong (next (t [ σ ]t)) tzmap)
   []f-id : {F : For Γₜ} → F [ idₜ {Γₜ} ]f ≡ F
+  []f-id {F = rel r tz} = cong (rel r) (≡tran (≡sym tzmap) []tz-id)
+  []f-id {F = F ⇒ G} = cong₂ _⇒_ []f-id []f-id
+  []f-id {F = ∀∀ F} = cong ∀∀ []f-id
+  llift-∘ : {α : Subt Ξₜ Δₜ} → {β : Subt Δₜ Γₜ} → llift (β ∘ₜ α) ≡ (llift β ∘ₜ lift α)
+  liftt[] : {α : Subt Δₜ Γₜ} → {t : Tm Γₜ} → liftt (t [ α ]t) ≡ (liftt t [ lift α ]t)
+  lifttz[] : {α : Subt Δₜ Γₜ} → {tz : Array (Tm Γₜ) n} → lifttz (tz [ α ]tz) ≡ (lifttz tz [ lift α ]tz)
+  llift-∘ {β = εₜ} = refl
+  llift-∘ {β = wk▹t β t} = cong₂ wk▹t llift-∘ (liftt[] {t = t})
+  liftt[] {t = fun f tz} = cong (fun f) lifttz[]
+  liftt[] {α = wk▹t α t} {var tvzero} = refl
+  liftt[] {α = wk▹t α t} {var (tvnext tv)} = liftt[] {t = var tv}
+  lifttz[] {tz = zero} = refl
+  lifttz[] {tz = next t tz} = cong₂ next (liftt[] {t = t}) lifttz[]
+  lift-∘ : {α : Subt Ξₜ Δₜ} → {β : Subt Δₜ Γₜ} → lift (β ∘ₜ α) ≡ (lift β) ∘ₜ (lift α)
+  lift-∘ {α = α} {β = εₜ} = refl
+  lift-∘ {α = α} {β = wk▹t β t} = cong₂ wk▹t (cong₂ wk▹t llift-∘ (liftt[] {t = t})) refl
   []f-∘ : {α : Subt Ξₜ Δₜ} → {β : Subt Δₜ Γₜ} → {F : For Γₜ} → F [ β ∘ₜ α ]f ≡ (F [ β ]f) [ α ]f
+  []f-∘ {α = α} {β = β} {F = rel r tz} = cong (rel r) (≡tran (≡tran (≡sym tzmap) (substP (λ tzz → (tz [ β ∘ₜ α ]tz) ≡ (tzz [ α ]tz)) tzmap []tz-∘)) tzmap)
+  []f-∘ {F = F ⇒ G} = cong₂ _⇒_ []f-∘ []f-∘
+  []f-∘ {F = ∀∀ F} = cong ∀∀ (≡tran (cong (λ σ → F [ σ ]f) lift-∘) []f-∘)
   rel[] : {σ : Subt Δₜ Γₜ} → {r : R n} → {tz : Array (Tm Γₜ) n} → (rel r tz) [ σ ]f ≡ rel r (map (λ t → t [ σ ]t) tz)
+  rel[] {r = r} = cong (rel r) refl
 
 
   
@@ -260,19 +298,22 @@ module FFOLInitial (F : Nat → Set) (R : Nat → Set) where
     ; πₜ²∘,ₜ = {!!}
     ; πₜ¹∘,ₜ = {!!}
     ; ,ₜ∘πₜ = {!!}
+    ; ,ₜ∘ = {!!}
     ; For = λ Γ → For (Con.t Γ)
     ; _[_]f = λ A σ → A [ subt σ ]f
-    ; []f-id = {!!}
-    ; []f-∘ = {!!}
+    ; []f-id = λ {Γ} {F} → []f-id {Con.t Γ} {F}
+    ; []f-∘ = {!λ {Γ Δ Ξ} {α} {β} {F} → []f-∘ {Con.t Γ} {Con.t Δ} {Con.t Ξ} {Sub.t α} {Sub.t β} {F}!}
     ; rel = rel
-    ; rel[] = {!!}
+    ; rel[] = rel[]
     ; _⊢_ = λ Γ A → Pf Γ A
+    ; _[_]p = {!!}
     ; _▹ₚ_ = _▹p_
     ; πₚ¹ = {!!}
     ; πₚ² = {!!}
     ; _,ₚ_ = {!!}
     ; ,ₚ∘πₚ = {!!}
     ; πₚ¹∘,ₚ = {!!}
+    ; ,ₚ∘ = {!!}
     ; _⇒_ = _⇒_
     ; []f-⇒ = {!!}
     ; ∀∀ = ∀∀
diff --git a/FinitaryFirstOrderLogic.agda b/FinitaryFirstOrderLogic.agda
index 2d869b4..cc5318d 100644
--- a/FinitaryFirstOrderLogic.agda
+++ b/FinitaryFirstOrderLogic.agda
@@ -8,10 +8,11 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
   open import ListUtil
 
   variable
-    ℓ¹ ℓ² ℓ³ ℓ⁴̂ ℓ⁵ : Level
+    ℓ¹ ℓ² ℓ³ ℓ⁴ ℓ⁵ : Level
     
-  record FFOL (F : Nat → Set) (R : Nat → Set) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴̂ ⊔ ℓ⁵)) where
+  record FFOL (F : Nat → Set) (R : Nat → Set) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴ ⊔ ℓ⁵)) where
     infixr 10 _∘_
+    infixr 5 _⊢_
     field
       Con : Set ℓ¹
       Sub : Con → Con → Set ℓ⁵ -- It makes a posetal category
@@ -38,6 +39,7 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
       πₜ²∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ² (σ ,ₜ t) ≡ t
       πₜ¹∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ¹ (σ ,ₜ t) ≡ σ
       ,ₜ∘πₜ : {Γ Δ : Con} → {σ : Sub Δ (Γ ▹ₜ)} → (πₜ¹ σ) ,ₜ (πₜ² σ) ≡ σ
+      ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t)
 
       -- Functor Con → Set called For
       For : Con → Set ℓ³
@@ -50,8 +52,8 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
       rel[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {n : Nat} → {r : R n} → {tz : Array (Tm Γ) n} → (rel r tz) [ σ ]f ≡ rel r (map (λ t → t [ σ ]t) tz)
 
       -- Proofs
-      _⊢_ : (Γ : Con) → For Γ → Prop ℓ⁴̂
-      --_[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) -- The functor's action on morphisms
+      _⊢_ : (Γ : Con) → For Γ → Prop ℓ⁴
+      _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) -- The functor's action on morphisms
       -- Equalities below are useless because Γ ⊢ F is in prop
       -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ id {Γ} ]p ≡ prf
       -- []p-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p
@@ -65,6 +67,7 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
       ,ₚ∘πₚ : {Γ Δ : Con} → {F : For Γ} → {σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ
       πₚ¹∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ¹ (σ ,ₚ prf) ≡ σ
       -- πₚ²∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ² (σ ,ₚ prf) ≡ prf
+      ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For Ξ}{prf : Γ ⊢ (F [ σ ]f)} → (σ ,ₚ prf) ∘ δ ≡ (σ ∘ δ) ,ₚ (substP (λ F → Δ ⊢ F) (≡sym []f-∘) (prf [ δ ]p))
 
 
       -- Implication
@@ -73,7 +76,7 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
 
       -- Forall
       ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ
-      []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → {t : Tm Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f))
+      []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f))
 
       -- Lam & App
       lam : {Γ : Con} → {F : For Γ} → {G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G)
@@ -84,6 +87,48 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
       ∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F)
       ∀e : {Γ : Con} → {F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f)
 
+
+    -- Examples
+    -- Proof utils
+    forall-in : {Γ Δ : Con} {σ : Sub Γ Δ} {A : For (Δ ▹ₜ)} → Γ ⊢ ∀∀ (A [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f) → Γ ⊢ (∀∀ A [ σ ]f)
+    forall-in {Γ = Γ} f = substP (λ F → Γ ⊢ F) (≡sym ([]f-∀∀)) f
+    wkₜ : {Γ : Con} → Sub (Γ ▹ₜ) Γ
+    wkₜ = πₜ¹ id
+    0ₜ : {Γ : Con} → Tm (Γ ▹ₜ)
+    0ₜ = πₜ² id
+    1ₜ : {Γ : Con} → Tm (Γ ▹ₜ ▹ₜ)
+    1ₜ = πₜ² (πₜ¹ id)
+    wkₚ : {Γ : Con} {A : For Γ} → Sub (Γ ▹ₚ A) Γ
+    wkₚ = πₚ¹ id
+    0ₚ : {Γ : Con} {A : For Γ} → Γ ▹ₚ A ⊢ A [ πₚ¹ id ]f
+    0ₚ = πₚ² id
+
+    --  Examples
+    ex0 : {A :  For ◇} → ◇ ⊢ (A ⇒ A)
+    ex0 {A = A} = lam 0ₚ
+    {-
+    ex1 : {A : For (◇ ▹ₜ)} → ◇ ⊢ ((∀∀ A) ⇒ (∀∀ A))
+    -- πₚ¹ id is adding an unused variable (syntax's llift)
+    ex1 {A = A} = lam (forall-in (∀i (substP (λ σ → ((◇ ▹ₚ ∀∀ A) ▹ₜ) ⊢ (A [ σ ]f)) {!!} {!!})))
+    -- (∀ x ∀ y . A(y,x)) ⇒ ∀ x ∀ y . A(x,y)
+    -- translation is (∀ ∀ A(0,1)) => (∀ ∀ A(1,0))
+    ex1' : {A : For (◇ ▹ₜ ▹ₜ)} → ◇ ⊢ ((∀∀ (∀∀ A)) ⇒ ∀∀ (∀∀ ( A [ (ε ,ₜ 0ₜ) ,ₜ 1ₜ ]f)))
+    ex1' = {!!}
+    -- (A ⇒ ∀ x . B(x)) ⇒ ∀ x . A ⇒ B(x)
+    ex2 : {A : For ◇} → {B : For (◇ ▹ₜ)} → ◇ ⊢ ((A ⇒ (∀∀ B)) ⇒ (∀∀ ((A [ wkₜ ]f) ⇒ B)))
+    ex2 = {!!}
+    -- ∀ x y . A(x,y) ⇒ ∀ x . A(x,x)
+    -- For simplicity, I swiched positions of parameters of A (somehow...)
+    ex3 : {A : For (◇ ▹ₜ ▹ₜ)} → ◇ ⊢ ((∀∀ (∀∀ A)) ⇒ (∀∀ (A [ id ,ₜ 0ₜ ]f)))
+    ex3 = {!!}
+    -- ∀ x . A (x) ⇒ ∀ x y . A(x)
+    ex4 : {A : For (◇ ▹ₜ)} → ◇ ⊢ ((∀∀ A) ⇒ (∀∀ (∀∀ (A [ ε ,ₜ 1ₜ ]f))))
+    ex4 = {!!}
+    -- (((∀ x . A (x)) ⇒ B)⇒ B) ⇒ ∀ x . ((A (x) ⇒ B) ⇒ B)
+    ex5 : {A : For (◇ ▹ₜ)} → {B : For ◇} → ◇ ⊢ ((((∀∀ A) ⇒ B) ⇒ B) ⇒ (∀∀ ((A ⇒ (B [ wkₜ ]f)) ⇒ (B [ wkₜ ]f))))
+    ex5 = {!!}
+    -}
+
   record Tarski : Set₁ where
     field
       TM : Set
@@ -145,6 +190,8 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
     πₜ¹∘,ₜ = refl
     ,ₜ∘πₜ : {Γ Δ : Con} → {σ : Sub Δ (Γ ▹ₜ)} → (πₜ¹ σ) ,ₜ (πₜ² σ) ≡ σ
     ,ₜ∘πₜ = refl
+    ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t)
+    ,ₜ∘ = refl
                                                                        
     -- Functor Con → Set called For
     For : Con → Set₁
@@ -181,7 +228,10 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
     ,ₚ∘πₚ : {Γ Δ : Con} → {F : For Γ} → {σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ
     ,ₚ∘πₚ = refl
     πₚ¹∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ¹ {Γ} {Δ} {F} (σ ,ₚ prf) ≡ σ
-    πₚ¹∘,ₚ = refl                                                                 
+    πₚ¹∘,ₚ = refl
+    ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For Ξ}{prf : Γ ⊢ (F [ σ ]f)} →
+      (_,ₚ_  {F = F} σ prf) ∘ δ ≡ (σ ∘ δ) ,ₚ (substP (λ F → Δ ⊢ F) (≡sym ([]f-∘ {α = δ} {β = σ} {F = F})) (prf [ δ ]p))
+    ,ₚ∘ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf} = refl
                                                                                                       
     -- Implication
     _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ
@@ -192,8 +242,8 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
     -- Forall
     ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ
     ∀∀ {Γ} F = λ (γ : Γ) → (∀ (t : TM) → F (γ ,× t))
-    []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → {t : Tm Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f))
-    []f-∀∀ {Γ} {Δ} {F} {σ} {t} = refl
+    []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f))
+    []f-∀∀ {Γ} {Δ} {F} {σ} = refl
                                                                                                                                         
     -- Lam & App
     lam : {Γ : Con} → {F : For Γ} → {G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G)
@@ -227,21 +277,24 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
             ; πₜ²∘,ₜ = λ {Γ} {Δ} {σ} → πₜ²∘,ₜ {Γ} {Δ} {σ}
             ; πₜ¹∘,ₜ = λ {Γ} {Δ} {σ} {t} → πₜ¹∘,ₜ {Γ} {Δ} {σ} {t}
             ; ,ₜ∘πₜ = ,ₜ∘πₜ
+            ; ,ₜ∘ = λ {Γ} {Δ} {Ξ} {σ} {δ} {t} → ,ₜ∘ {Γ} {Δ} {Ξ} {σ} {δ} {t}
             ; For = For
             ; _[_]f = _[_]f
             ; []f-id = []f-id
             ; []f-∘ = λ {Γ} {Δ} {Ξ} {α} {β} {F} → []f-∘ {Γ} {Δ} {Ξ} {α} {β} {F}
             ; _⊢_ = _⊢_
+            ; _[_]p = _[_]p
             ; _▹ₚ_ = _▹ₚ_
             ; πₚ¹ = πₚ¹
             ; πₚ² = πₚ²
             ; _,ₚ_ = _,ₚ_
             ; ,ₚ∘πₚ = ,ₚ∘πₚ
             ; πₚ¹∘,ₚ = λ {Γ} {Δ} {F} {σ} {p} → πₚ¹∘,ₚ {Γ} {Δ} {F} {σ} {p}
+            ; ,ₚ∘ = λ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf} → ,ₚ∘ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf}
             ; _⇒_ = _⇒_
             ; []f-⇒ = λ {Γ} {F} {G} {σ} → []f-⇒ {Γ} {F} {G} {σ}
             ; ∀∀ = ∀∀
-            ; []f-∀∀ = λ {Γ} {Δ} {F} {σ} {t} → []f-∀∀ {Γ} {Δ} {F} {σ} {t}
+            ; []f-∀∀ = λ {Γ} {Δ} {F} {σ} → []f-∀∀ {Γ} {Δ} {F} {σ}
             ; lam = lam
             ; app = app
             ; ∀i = ∀i
@@ -341,6 +394,8 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
     πₜ¹∘,ₜ = refl
     ,ₜ∘πₜ : {Γ Δ : Con} → {σ : Sub Δ (Γ ▹ₜ)} → (πₜ¹ σ) ,ₜ (πₜ² σ) ≡ σ
     ,ₜ∘πₜ = refl
+    ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t)
+    ,ₜ∘ = refl
                                                                     
     -- Functor Con → Set called For
     For : Con → Set₁
@@ -381,6 +436,10 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
     ,ₚ∘πₚ = refl
     πₚ¹∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ¹ {Γ} {Δ} {F} (σ ,ₚ prf) ≡ σ
     πₚ¹∘,ₚ = refl
+    ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For Ξ}{prf : Γ ⊢ (F [ σ ]f)} →
+      (_,ₚ_  {F = F} σ prf) ∘ δ ≡ (σ ∘ δ) ,ₚ (substP (λ F → Δ ⊢ F) (≡sym ([]f-∘ {α = δ} {β = σ} {F = F})) (prf [ δ ]p))
+    ,ₚ∘ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf} = refl
+    
                                                                                                       
                                                                                                       
     -- Implication
@@ -392,7 +451,7 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
     -- Forall
     ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ
     ∀∀ F = λ w → λ γ → ∀ t → F w (γ ,× t)
-    []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → {t : Tm Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f))
+    []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f))
     []f-∀∀ = refl
                                                                                                                            
     -- Lam & App
@@ -428,21 +487,24 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
       ; πₜ²∘,ₜ = λ {Γ} {Δ} {σ} → πₜ²∘,ₜ {Γ} {Δ} {σ}
       ; πₜ¹∘,ₜ = λ {Γ} {Δ} {σ} {t} → πₜ¹∘,ₜ {Γ} {Δ} {σ} {t}
       ; ,ₜ∘πₜ = ,ₜ∘πₜ
+      ; ,ₜ∘ = λ {Γ} {Δ} {Ξ} {σ} {δ} {t} → ,ₜ∘ {Γ} {Δ} {Ξ} {σ} {δ} {t}
       ; For = For
       ; _[_]f = _[_]f
       ; []f-id = []f-id
       ; []f-∘ = λ {Γ} {Δ} {Ξ} {α} {β} {F} → []f-∘ {Γ} {Δ} {Ξ} {α} {β} {F}
       ; _⊢_ = _⊢_
+      ; _[_]p = _[_]p
       ; _▹ₚ_ = _▹ₚ_
       ; πₚ¹ = πₚ¹
       ; πₚ² = πₚ²
       ; _,ₚ_ = _,ₚ_
       ; ,ₚ∘πₚ = ,ₚ∘πₚ
       ; πₚ¹∘,ₚ = λ {Γ} {Δ} {F} {σ} {p} → πₚ¹∘,ₚ {Γ} {Δ} {F} {σ} {p}
+      ; ,ₚ∘ = λ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf} → ,ₚ∘ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf}
       ; _⇒_ = _⇒_
       ; []f-⇒ = λ {Γ} {F} {G} {σ} → []f-⇒ {Γ} {F} {G} {σ}
       ; ∀∀ = ∀∀
-      ; []f-∀∀ = λ {Γ} {Δ} {F} {σ} {t} → []f-∀∀ {Γ} {Δ} {F} {σ} {t}
+      ; []f-∀∀ = λ {Γ} {Δ} {F} {σ} → []f-∀∀ {Γ} {Δ} {F} {σ}
       ; lam = lam
       ; app = app
       ; ∀i = ∀i
diff --git a/PropUtil.agda b/PropUtil.agda
index 9d36f9c..93c498f 100644
--- a/PropUtil.agda
+++ b/PropUtil.agda
@@ -61,6 +61,9 @@ module PropUtil where
   ≡sym : {ℓ : Level} → {A : Set ℓ}→ {a a' : A} → a ≡ a' → a' ≡ a
   ≡sym refl = refl
 
+  ≡tran : {ℓ : Level} {A : Set ℓ} → {a a' a'' : A} → a ≡ a' → a' ≡ a'' → a ≡ a''
+  ≡tran refl refl = refl
+
   postulate ≡fun : {ℓ ℓ' : Level} → {A : Set ℓ} → {B : Set ℓ'} → {f g : A → B} → ((x : A) → (f x ≡ g x)) → f ≡ g
   postulate ≡fun' : {ℓ ℓ' : Level} → {A : Set ℓ} → {B : A → Set ℓ'} → {f g : (a : A) → B a} → ((x : A) → (f x ≡ g x)) → f ≡ g
 
@@ -70,6 +73,11 @@ module PropUtil where
   postulate substrefl   : ∀{ℓ}{A : Set ℓ}{ℓ'}{P : A → Set ℓ'}{a : A}{e : a ≡ a}{p : P a} → subst P e p ≈ p
   {-# REWRITE substrefl   #-}
 
+  cong : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'} → (f : A → B) → {a a' : A} → a ≡ a' → f a ≡ f a'
+  cong f refl = refl
+  cong₂ : {ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''} → (f : A → B → C) → {a a' : A} {b b' : B} → a ≡ a' → b ≡ b' → f a b ≡ f a' b'
+  cong₂ f refl refl = refl
+
   {-# BUILTIN EQUALITY _≡_ #-}
 
   data Nat : Set where