open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq renaming ([_] to [_]ᵢ) 
open import Function hiding (_↔_)
open import Function.Equality hiding (id; cong; _∘_; flip)
open import Function.Inverse hiding (id; sym; map; _∘_; _↔_)
open import Data.List as List hiding (any) renaming (length to length')
open import Data.List.Properties
open import Data.List.Relation.Unary.Any as Any hiding (map)
open import Data.List.Relation.Unary.Any.Properties  
open import Data.List.Relation.Binary.Subset.Propositional
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Data.Bool hiding (_≟_;_∨_)
open import Data.Nat as Nat hiding (_*_; _≟_)
open import Data.Sum hiding (map)
open import Data.Empty
open import Data.Maybe hiding (map)
open import Data.Product as Prod renaming (Σ to Σₓ;map to mapₓ) 
open import Relation.Nullary
open import Relation.Nullary.Decidable hiding (map)
open import Relation.Nullary.Negation
open import Algebra.Structures

open import Stoughton.Var

module Stoughton.Substitution (𝒞 : Set) {𝒱 : Set} (var : Enum 𝒱) where

  private 
    _≟_ = Enum._≟_ var

  open import Stoughton.Chi (Enum.encode var) (Enum.decode var) (Enum.inverse var)
  open import Stoughton.Syntax 𝒞 𝒱 _≟_

  infixl  _⊙_
  infixl  _[_:=_]
  infixl  [_/_]_
  
  Sub : Set
  Sub = 𝒱 → Λ

  ι : Sub
  ι = v

  infixl  _‚_:=_ 
  _‚_:=_ : Sub → 𝒱 → Λ → Sub
  (σ ‚ x := M) y with x ≟ y
  ... | yes _ = M
  ... | no  _ = σ y

  x≢y→x[y/M]≡x : {x y : 𝒱}{M : Λ} → x ≢ y → (ι ‚ x := M) y ≡ v y
  x≢y→x[y/M]≡x {x} {y} x≢y with x ≟ y
  ... | yes x≡y = ⊥-elim (x≢y x≡y)
  ... | no  _   = refl

  Res : Set
  Res = Sub × List 𝒱

  _#⇂_ : 𝒱 → Res → Set
  x #⇂ (σ , xs) = ∀ y → y ∈ xs → x # σ y

  #∈⇒#∈- : ∀ {x y l σ} → x #⇂ (σ , l) → x #⇂ (σ , l - y)
  #∈⇒#∈- x#σ⇂xs = λ x x*xs-y → x#σ⇂xs x (∈-→∈ x*xs-y)
  
  lemma#→ι#⇂ : ∀ {x y l} → x ∉ l - y → x #⇂ (ι , l - y)
  lemma#→ι#⇂ {x} {y} {M} x∉xs-y z z∈xs-y with z ≟ x
  ... | no z≢x = λ { (here x=z) → z≢x (sym x=z) } 
  lemma#→ι#⇂ {x} {y} {M} z∉xs-y .x z∈xs-y | yes refl = ⊥-elim (z∉xs-y z∈xs-y)

  #++⁻ : ∀ {x σ xs ys} → x #⇂ (σ , xs ++ ys) → x #⇂ (σ , xs) × x #⇂ (σ , ys)
  #++⁻ {_} {_} {xs} x#σ⇂xs++ys = (λ y y∈xs → x#σ⇂xs++ys y (∈-++⁺ˡ y∈xs)) , (λ y y∈ys → x#σ⇂xs++ys y (∈-++⁺ʳ xs y∈ys))

  _*⇂_ : 𝒱 → Res → Set 
  x *⇂ (σ , xs) = ∃ λ y → y ∈ xs × x * σ y
  
  infix  _≅σ_
  _≅σ_ : Sub → Sub → Set
  σ ≅σ σ' = (x : 𝒱) → σ x ≡ σ' x

  lemmaσ≺+x,x≅σ : {x : 𝒱} → ι ‚ x := v x ≅σ ι
  lemmaσ≺+x,x≅σ {x} y with x ≟ y
  ... | no   _     = refl
  lemmaσ≺+x,x≅σ {x} .x
      | yes  refl  = refl

  _≅⇂ₗ_ : Res → Res → Set
  (σ , xs) ≅⇂ₗ (σ' , xs') = (xs ≈ xs') × (∀ x → x ∈ xs → σ x ≡ σ' x)

  _≅_⇂_ : Sub → Sub → List 𝒱 → Set
  σ ≅ σ' ⇂ xs = (σ , xs) ≅⇂ₗ (σ' , xs)

  lemma≅≺+ : {x : 𝒱}{N : Λ}{σ σ' : Sub} → σ ≅σ σ' → σ ‚ x := N ≅σ σ' ‚ x := N
  lemma≅≺+ {x} σ≌σ' y with x ≟ y
  ... | yes  _ = refl 
  ... | no   _ = σ≌σ' y

  prop6 : {σ σ' : Sub}{M : List 𝒱} → σ ≅σ σ' → σ ≅ σ' ⇂ M
  prop6 σ≅σ' = ∼*ρ , λ x _ → σ≅σ' x

  _∼*⇂_ : Res → Res → Set
  (σ , xs) ∼*⇂ (σ' , xs') =  (∀ x → x *⇂ (σ , xs) → x *⇂ (σ' , xs')) × (∀ x → x *⇂ (σ' , xs') → x *⇂ (σ , xs))
  
  private 
    lemmafilter→ : (x : 𝒱)(xs : List 𝒱)(p : 𝒱 → Bool) → x ∈ boolFilter p xs → (p x ≡ true × x ∈ xs)
    lemmafilter→ x []        p ()
    lemmafilter→ x (y ∷ xs)  p x∈filterpy∷xs with p y | inspect p y
    ...  | false   | [ py≡false ]ᵢ = mapₓ id there (lemmafilter→ x xs p x∈filterpy∷xs)
    lemmafilter→ x (.x ∷ xs) p (here refl)         | true | [ px≡true ]ᵢ = px≡true , here refl
    lemmafilter→ x (y ∷ xs) p (there x∈filterpxs)  | true | [ py≡true ]ᵢ = mapₓ id there (lemmafilter→ x xs p x∈filterpxs)

  X : Res → 𝒱
  X (σ , xs) = X' (concat (map (fv ∘ σ) xs))

  χₜ : Λ → 𝒱
  χₜ M = X' (fv M)

  Xfresh : ∀ σ xs → X (σ , xs) #⇂ (σ , xs)
  Xfresh σ xs y y∈xs χσ⇂xs∈σy = ⊥-elim (χ∉concatmapfv∘σfvM χ∈concatmapfv∘σfvM)
    where
    χ∉concatmapfv∘σfvM : X (σ , xs) ∉ (concat (map (fv ∘ σ) xs))
    χ∉concatmapfv∘σfvM = Xpfresh (concat (map (fv ∘ σ) xs))
    fvσy∈mapfv∘σfvM : fv (σ y) ∈ map (fv ∘ σ) xs
    fvσy∈mapfv∘σfvM = Π._⟨$⟩_ (Inverse.to (map-∈↔ (fv ∘ σ))) (y , y∈xs , refl)
    χ∈concatmapfv∘σfvM : X (σ , xs) ∈ (concat (map (fv ∘ σ) xs))
    χ∈concatmapfv∘σfvM = Π._⟨$⟩_ (Inverse.to (concat-∈↔ {xss = map (fv ∘ σ) xs})) (fv (σ y) ,  χσ⇂xs∈σy , fvσy∈mapfv∘σfvM)

  Xfn : (σ σ' : Sub)(M M' : List 𝒱) → (σ , M) ∼*⇂ (σ' , M') → X (σ , M) ≡ X (σ' , M')
  Xfn σ σ' M M' (h1 , h2) = lemmaχaux⊆ (concat (map (fv ∘ σ) M)) (concat (map (fv ∘ σ') M')) lemma⊆ lemma⊇
    where
    lemma⊆ : concat (map (fv ∘ σ) M) ⊆ concat (map (fv ∘ σ') M')
    lemma⊆ {y} y∈concat with Π._⟨$⟩_ (Inverse.from (concat-∈↔ {xss = map (fv ∘ σ) M})) y∈concat 
    ... | xs , y∈xs , xs∈map with Π._⟨$⟩_ (Inverse.from ((map-∈↔ (fv ∘ σ) {xs = M}))) xs∈map
    lemma⊆ {y} y∈concat | .(fv (σ x)) , y∈fvσx , fvσx∈map | x , x∈fvM , refl with h1 y (x , x∈fvM , y∈fvσx) 
    ... | u , ufreeM' , yfreeσ'u with Π._⟨$⟩_ (Inverse.to ((map-∈↔ (fv ∘ σ') {y = fv (σ' u)} {xs = M'}))) (u , ufreeM' , refl) 
    ... | fvσ'u∈map = Π._⟨$⟩_ (Inverse.to (concat-∈↔ {xss = map (fv ∘ σ') M'})) (fv (σ' u) , yfreeσ'u , fvσ'u∈map) 
    lemma⊇ : concat (map (fv ∘ σ') M') ⊆ (concat (map (fv ∘ σ) M))
    lemma⊇ {y} y∈concat with Π._⟨$⟩_ (Inverse.from (concat-∈↔ {xss = map (fv ∘ σ') M'})) y∈concat 
    ... | xs , y∈xs , xs∈map with Π._⟨$⟩_ (Inverse.from ((map-∈↔ (fv ∘ σ') {xs = M'}))) xs∈map
    lemma⊇ {y} y∈concat | .(fv (σ' x)) , y∈fvσ'x , fvσ'x∈map | x , x∈fvM' , refl with h2 y (x , x∈fvM' , y∈fvσ'x) 
    ... | u , ufreeM , yfreeσu with Π._⟨$⟩_ (Inverse.to ((map-∈↔ (fv ∘ σ) {y = fv (σ u)} {xs = M}))) (u , ufreeM , refl) 
    ... | fvσu∈map = Π._⟨$⟩_ (Inverse.to (concat-∈↔ {xss = map (fv ∘ σ) M})) (fv (σ u) , yfreeσu , fvσu∈map) 

  concat-map-ι : ∀ xs → concat (List.map (fv ∘ ι) xs) ≡ xs
  concat-map-ι [] = refl
  concat-map-ι (x ∷ xs) = cong (_∷_ x) (concat-map-ι xs)
  
  lemma-χιₗ : (xs : List 𝒱) → X (ι , xs) ∉ xs
  lemma-χιₗ xs rewrite concat-map-ι xs = Xpfresh xs

  infixl  _∙_
  _∙_ : Λ → Sub → Λ
  c k ∙ σ = c k
  v x ∙ σ = σ x
  M · N ∙ σ = (M ∙ σ) · (N ∙ σ)
  λ[ x ∶ A ] M ∙ σ = λ[ y ∶ A ∙ σ ](M ∙ σ ‚ x := v y) where y = X (σ , fv M - x)
  Π[ x ∶ A ] B ∙ σ = Π[ y ∶ A ∙ σ ](B ∙ σ ‚ x := v y) where y = X (σ , fv B - x)

  _⊙_ : Sub → Sub → Sub
  (σ ⊙ σ') x = (σ' x) ∙ σ

  lemmaι : {σ : Sub} → σ ≅σ σ ⊙ ι
  lemmaι x = refl

  prop7 : {x : 𝒱}{σ σ' : Sub}{M : Λ} → (σ' ⊙ σ) ‚ x := (M ∙ σ') ≅σ σ' ⊙ (σ ‚ x := M)
  prop7 {x} {σ} {σ'} {M} y with x ≟ y
  ... | yes _  = refl
  ... | no _   = refl

  lemmax∙ι≺+x,N : (x : 𝒱)(N : Λ) → v x ∙ ι ‚ x := N ≡ N  
  lemmax∙ι≺+x,N x N with x ≟ x 
  ... | yes  _    = refl
  ... | no   x≢x  = ⊥-elim (x≢x refl) 

  lemmafreeσ→ₗ : ∀ {x M σ} → x ∈ fv (M ∙ σ) → x *⇂ (σ , fv M)
  lemmafreeσ→ₗ {x} {c _}   {σ} ()
  lemmafreeσ→ₗ {x} {v z}   {σ} xfreeσz = z , here refl , xfreeσz
  lemmafreeσ→ₗ {x} {M · N} {σ} xfreeMNσ with ∈-++⁻ (fv (M ∙ σ)) xfreeMNσ
  ... | inj₁ xfreeMσ = Prod.map₂ (Prod.map₁ ∈-++⁺ˡ) (lemmafreeσ→ₗ {x} {M} xfreeMσ)
  ... | inj₂ xfreeNσ = Prod.map₂ (Prod.map₁ (∈-++⁺ʳ (fv M))) (lemmafreeσ→ₗ {x} {N} xfreeNσ)
  lemmafreeσ→ₗ {x} {λ[ y ∶ A ] M} {σ} xfreeλy:AMσ with ∈-++⁻ (fv (A ∙ σ)) xfreeλy:AMσ
  ... | inj₁ x*Aσ with lemmafreeσ→ₗ {x} {A} x*Aσ
  ... | y , y*A , σx*y = y , ∈-++⁺ˡ y*A , σx*y   
  lemmafreeσ→ₗ {x} {λ[ y ∶ A ] M} {σ} xfreeλy:AMσ | inj₂ xfreeMσ<+yz-z with lemmafreeσ→ₗ {x} {M} xfreeMσ<+yz
    where
    z : 𝒱
    z = X (σ , fv M - y)
    xfreeMσ<+yz : x * M ∙ σ ‚ y := v z
    xfreeMσ<+yz = ∈-→∈ xfreeMσ<+yz-z
  ... | w , wfreeM , xfreeσ<+yzw with y ≟ w
  ... | no  y≢w = w , ∈-++⁺ʳ (fv A) (lemma∈-≢ wfreeM y≢w) , xfreeσ<+yzw
  lemmafreeσ→ₗ {x} {λ[ y ∶ A ] M} {σ} xfreeλy:AMσ | inj₂ xfreeMσ<+yz-z | w , _ , here x=z | yes y=w = ⊥-elim (x≢z x=z)
    where
    z : 𝒱
    z = X (σ , fv M - y)    
    x≢z : x ≢ z
    x≢z = ∈-→≢ {xs = fv (M ∙ σ ‚ y := v z)} xfreeMσ<+yz-z
  lemmafreeσ→ₗ {x} {Π[ y ∶ A ] M} {σ} xfreeΠy:AMσ with ∈-++⁻ (fv (A ∙ σ)) xfreeΠy:AMσ
  ... | inj₁ x*Aσ with lemmafreeσ→ₗ {x} {A} x*Aσ
  ... | y , y*A , σx*y = y , ∈-++⁺ˡ y*A , σx*y   
  lemmafreeσ→ₗ {x} {Π[ y ∶ A ] M} {σ} xfreeΠy:AMσ | inj₂ xfreeMσ<+yz-z with lemmafreeσ→ₗ {x} {M} xfreeMσ<+yz
    where
    z : 𝒱
    z = X (σ , fv M - y)
    xfreeMσ<+yz : x * M ∙ σ ‚ y := v z
    xfreeMσ<+yz = ∈-→∈ xfreeMσ<+yz-z
  ... | w , wfreeM , xfreeσ<+yzw with y ≟ w
  ... | no  y≢w = w , ∈-++⁺ʳ (fv A) (lemma∈-≢ wfreeM y≢w) , xfreeσ<+yzw
  lemmafreeσ→ₗ {x} {Π[ y ∶ A ] M} {σ} xfreeΠy:AMσ | inj₂ xfreeMσ<+yz-z | w , _ , here x=z | yes y=w = ⊥-elim (x≢z x=z)
    where
    z : 𝒱
    z = X (σ , fv M - y)    
    x≢z : x ≢ z
    x≢z = ∈-→≢ {xs = fv (M ∙ σ ‚ y := v z)} xfreeMσ<+yz-z    
  
  lemmafreeσ←ₗ : {x : 𝒱}{M : Λ}{σ : Sub} → x *⇂ (σ , fv M) → x ∈ fv (M ∙ σ)
  lemmafreeσ←ₗ {x} {v z}   {σ} (.z , here refl       , xfreeσz) = xfreeσz
  lemmafreeσ←ₗ {x} {M · N} {σ} (y  , y*MN    , xfreeσy) with ∈-++⁻ (fv M) y*MN
  ... | inj₁ yfreeM = ∈-++⁺ˡ {ys = fv (N ∙ σ)} (lemmafreeσ←ₗ {M = M} (y , yfreeM , xfreeσy))
  ... | inj₂ yfreeN = ∈-++⁺ʳ (fv (M ∙ σ)) (lemmafreeσ←ₗ {M = N} (y , yfreeN , xfreeσy))
  lemmafreeσ←ₗ {x} {λ[ z ∶ A ] M} {σ} (y  , y*AM-z , xfreeσy) with ∈-++⁻ (fv A) y*AM-z
  ... | inj₁ y*A = ∈-++⁺ˡ (lemmafreeσ←ₗ {x} {A} {σ} (y , y*A , xfreeσy))
  ... | inj₂ y*M-z with X (σ , fv M - z) | (Xfresh σ (fv M - z)) y y*M-z
  ... | w | w#σy with w ≟ x
  ... | no  w≢x = ∈-++⁺ʳ (fv (A ∙ σ)) (lemma∈-≢ (lemmafreeσ←ₗ {x} {M} (y , (∈-→∈ y*M-z) , lemma)) w≢x) 
    where
    lemma :  x ∈ fv ((σ ‚ z := v w) y)
    lemma with z ≟ y 
    ... | yes z≡y = ⊥-elim ((∈-→≢ {xs = fv M} y*M-z) (sym z≡y))
    ... | no  _   = xfreeσy
  lemmafreeσ←ₗ {x} {λ[ z ∶ A ] M} {σ} (y  , _ , xfreeσy) | inj₂ y*M-z | .x | x#σy | yes refl = ⊥-elim (x#σy xfreeσy)
  lemmafreeσ←ₗ {x} {Π[ z ∶ A ] M} {σ} (y  , y*AM-z , xfreeσy) with ∈-++⁻ (fv A) y*AM-z
  ... | inj₁ y*A = ∈-++⁺ˡ (lemmafreeσ←ₗ {x} {A} {σ} (y , y*A , xfreeσy))
  ... | inj₂ y*M-z with X (σ , fv M - z) | (Xfresh σ (fv M - z)) y y*M-z
  ... | w | w#σy with w ≟ x
  ... | no  w≢x = ∈-++⁺ʳ (fv (A ∙ σ)) (lemma∈-≢ (lemmafreeσ←ₗ {x} {M} (y , (∈-→∈ y*M-z) , lemma)) w≢x) 
    where
    lemma :  x ∈ fv ((σ ‚ z := v w) y)
    lemma with z ≟ y 
    ... | yes z≡y = ⊥-elim ((∈-→≢ {xs = fv M} y*M-z) (sym z≡y))
    ... | no  _   = xfreeσy
  lemmafreeσ←ₗ {x} {Π[ z ∶ A ] M} {σ} (y  , _ , xfreeσy) | inj₂ y*M-z | .x | x#σy | yes refl = ⊥-elim (x#σy xfreeσy)

  noCapture : ∀ {x M σ} → x ∈ fv (M ∙ σ) ↔ x *⇂ (σ , fv M)
  noCapture {x} {M} {σ} = lemmafreeσ→ₗ {x} {M} {σ} , lemmafreeσ←ₗ {x} {M} {σ}

  --lemmafreshσ→ₗ : ∀ {x M σ} → x ∉ fv (M ∙ σ) → x #⇂ (σ , fv M)
  --lemmafreshσ→ₗ x∉fvMσ z z∈fvM = {!!}

  ∼*⇒∼*⇂ : ∀ {σ σ' xs xs'} → (∀ x → x ∈ xs → fv (σ x) ≈ fv (σ' x)) → xs ≈ xs' → (σ , xs) ∼*⇂ (σ' , xs')
  ∼*⇒∼*⇂ {σ} {σ'} {xs} {xs'} x*M⇛σx∼σ'x (*M⇒M' , *M'⇒M) = h1 , h2
    where 
    h1 : (y : 𝒱) → ∃ (λ x → (x ∈ xs)  × (y * σ x))  → ∃ (λ u → (u ∈ xs') × (y * σ' u))
    h1 y (x , x*M , y*σx)    =  x , *M⇒M' x*M , proj₁ (x*M⇛σx∼σ'x x x*M) y*σx
    h2 : (y : 𝒱) → ∃ (λ x → (x ∈ xs') × (y * σ' x)) → ∃ (λ u → (u ∈ xs) ×  (y * σ u)) 
    h2 y (x , x*M' , y*σ'x)  =  x , *M'⇒M x*M' , proj₂ (x*M⇛σx∼σ'x x (*M'⇒M x*M')) y*σ'x 

  subEqRes : ∀ {M σ σ'} → σ ≅ σ' ⇂ fv M → M ∙ σ ≡ M ∙ σ'
  subEqRes {c k}   {σ} {σ'} (_ , f) = refl
  subEqRes {v x}   {σ} {σ'} (_ , f) = f x (here refl)
  subEqRes {M · N} {σ} {σ'} (_ , f)  =
    cong₂ _·_ (subEqRes {M} (((λ x → x) , (λ x → x)) , (λ x xfreeM → f x (∈-++⁺ˡ xfreeM)))) (subEqRes {N} (((λ x → x) , (λ x → x)) , (λ x xfreeN → f x (∈-++⁺ʳ (fv M) xfreeN))))
  subEqRes {λ[ x ∶ A ] M} {σ} {σ'} (_ , f)
    with X (σ , fv M - x) | X (σ' , fv M - x) | Xfn σ σ' (fv M - x) (fv M - x) (∼*⇒∼*⇂ {σ} {σ'} (λ x x*M → (lemma-1 x x*M) , (lemma-2 x x*M)) (id , id)) 
    where 
    lemma-1 : (w : 𝒱) → w ∈ fv M - x → {z : 𝒱} → z ∈ fv (σ w) → z ∈ fv (σ' w)
    lemma-1 w wfreeλxM {z} zfreeσw rewrite f w (∈-++⁺ʳ (fv A) wfreeλxM) = zfreeσw
    lemma-2 : (w : 𝒱) → w ∈ fv M - x → {z : 𝒱} → z ∈ fv (σ' w) → z ∈ fv (σ w)
    lemma-2 w wfreeλxM {z} zfreeσ'w rewrite f w (∈-++⁺ʳ (fv A) wfreeλxM) = zfreeσ'w
  ... | y | .y | refl = cong₂ (λ[_∶_]_ y) (subEqRes {A} ((id , id) , λ w w*A → f w (∈-++⁺ˡ w*A))) (subEqRes {M} ((id , id) , lemma)) 
    where 
    lemma : ((z : 𝒱) → z * M → (σ ‚ x := v y) z ≡ (σ' ‚ x := v y) z)
    lemma z zfreeM with x ≟ z 
    ... | yes _   = refl
    ... | no  x≢z = f z (∈-++⁺ʳ (fv A) (lemma∈-≢ zfreeM x≢z))
  subEqRes {Π[ x ∶ A ] M} {σ} {σ'} (_ , f)
    with X (σ , fv M - x) | X (σ' , fv M - x) | Xfn σ σ' (fv M - x) (fv M - x) (∼*⇒∼*⇂ {σ} {σ'} (λ x x*M → (lemma-1 x x*M) , (lemma-2 x x*M)) (id , id)) 
    where 
    lemma-1 : (w : 𝒱) → w ∈ fv M - x → {z : 𝒱} → z ∈ fv (σ w) → z ∈ fv (σ' w)
    lemma-1 w wfreeλxM {z} zfreeσw rewrite f w (∈-++⁺ʳ (fv A) wfreeλxM) = zfreeσw
    lemma-2 : (w : 𝒱) → w ∈ fv M - x → {z : 𝒱} → z ∈ fv (σ' w) → z ∈ fv (σ w)
    lemma-2 w wfreeλxM {z} zfreeσ'w rewrite f w (∈-++⁺ʳ (fv A) wfreeλxM) = zfreeσ'w
  ... | y | .y | refl = cong₂ (Π[_∶_]_ y) (subEqRes {A} ((id , id) , λ w w*A → f w (∈-++⁺ˡ w*A))) (subEqRes {M} ((id , id) , lemma)) 
    where 
    lemma : ((z : 𝒱) → z * M → (σ ‚ x := v y) z ≡ (σ' ‚ x := v y) z)
    lemma z zfreeM with x ≟ z 
    ... | yes _   = refl
    ... | no  x≢z = f z (∈-++⁺ʳ (fv A) (lemma∈-≢ zfreeM x≢z))    

  _[_:=_] : Λ → 𝒱 → Λ → Λ
  M [ x := N ] = M ∙ ι ‚ x := N 

  [_/_]_ : Λ → 𝒱 → Λ → Λ
  [ N / x ] M = M ∙ ι ‚ x := N 
  
  lemma≺+≡ : ∀ {m x σ M} → m ≡ x → (σ ‚ m := M) x ≡ M
  lemma≺+≡ {m} {x} m≡x with m ≟ x
  ... | yes _ = refl
  ... | no m≢x = ⊥-elim (m≢x m≡x)

  lemma≺+≡′ : (σ : Sub) → (x : 𝒱) → ∀ {M} → (σ ‚ x := M) x ≡ M
  lemma≺+≡′ σ x = lemma≺+≡ {x} {x} refl

  lemma≺+≢ : ∀ {σ M m x} → m ≢ x → (σ ‚ m := M) x ≡ σ x
  lemma≺+≢ {_} {_} {m} {x} m≢x with m ≟ x
  ... | yes m≡x = ⊥-elim (m≢x m≡x)
  ... | no _ = refl

  updFresh : ∀ {x M N σ} → x # M → M ∙ (σ ‚ x := N) ≡ M ∙ σ
  updFresh {x} {M} {N} {σ} x#M = subEqRes {M} (∼*ρ , h)
    where
      h : (y : 𝒱) → y ∈ fv M → (σ ‚ x := N) y ≡ σ y
      h y y*M with x ≟ y
      h .x x*M | yes refl = ⊥-elim (x#M x*M)
      h _ _ | no _ = refl

  lemmaMι≺+x,x : {x : 𝒱}{M : Λ} → M ∙ ι ‚ x := v x ≡ M ∙ ι
  lemmaMι≺+x,x {x} {M} = subEqRes {M} (prop6 {ι ‚ x := v x} {ι} (lemmaσ≺+x,x≅σ {x})) 

  open PropEq.≡-Reasoning renaming (begin_ to begin≡_;_∎ to _◻)

  lemmaσ∘≺+ : (M N : Λ)(σ σ' : Sub)(x y : 𝒱) → y #⇂ (σ , fv M - x) → (w : 𝒱) → w ∈ fv M → ((σ' ‚ y := N) ⊙ (σ ‚ x := v y)) w ≡ ((σ' ⊙ σ) ‚ x := N) w
  lemmaσ∘≺+ M N σ σ' x y y#⇂σ,λxM w wfreeM with x ≟ w
  ... | no  x≢w =
    begin≡
    (σ w) ∙ (σ' ‚ y := N)
    ≡⟨ subEqRes {σ w} {σ' ‚ y := N} {σ'} (∼*ρ , lemma) ⟩ 
    (σ w) ∙ σ'
    ◻
    where 
    lemma : (u : 𝒱) → u ∈ fv (σ w) → (σ' ‚ y := N) u ≡ σ' u
    lemma u ufreeσw with y#⇂σ,λxM w (lemma∈-≢ wfreeM x≢w)
    ... | y#σw with y ≟ u
    ...        | no  _    = refl
    lemma .y yfreeσw | y#σw | yes refl = ⊥-elim (y#σw yfreeσw)
  ... | yes x≡w with y ≟ y
  ... | yes y≡y = refl 
  ... | no  y≢y = ⊥-elim (y≢y refl)           

  lemmaχσ∘≺+ : (M N : Λ)(σ σ' : Sub)(x : 𝒱) → (w : 𝒱) → w ∈ fv M → ((σ' ‚ X (σ , fv M - x) := N) ⊙ (σ ‚ x := v (X (σ , fv M - x)))) w ≡ ((σ' ⊙ σ) ‚ x := N) w
  lemmaχσ∘≺+ M N σ σ' x = lemmaσ∘≺+ M N σ σ' x (X (σ , fv M - x)) (Xfresh σ (fv M - x)) 

  lemma3-1 : ∀ {x M σ σ'} → X (σ' , fv (M ∙ (σ ‚ x := v (X (σ , fv M - x)))) - X (σ , fv M - x)) ≡ X (σ' ⊙ σ , fv M - x)
  lemma3-1 {x} {M} {σ} {σ'} = Xfn σ' (σ' ⊙ σ) (fv (M ∙ (σ ‚ x := v y)) - y) (fv M - x) (lemma3→ , lemma3←) 
    where
    y = X (σ , fv M - x)
    y' = X (σ' , fv (M ∙ (σ ‚ x := v y)) - y)
    z = X (σ' ⊙ σ , fv M - x)
    lemma3→ : (y' : 𝒱) → y' *⇂ (σ' , fv (M ∙ σ ‚ x := v y) - y) → y' *⇂ (σ' ⊙ σ , fv M - x)
    lemma3→ y' (x' , x'freeMσ≺+xy-y , y'freeσ'x') with lemmafreeσ→ₗ {x'} {M} (∈-→∈ x'freeMσ≺+xy-y) 
    ... | u , ufreeM , x'freeσ≺+xyu with x ≟ u
    ... | no  x≢u = u , lemma∈-≢ ufreeM x≢u , lemmafreeσ←ₗ {y'} {σ u} {σ'} (x' , x'freeσ≺+xyu , y'freeσ'x') 
    lemma3→ y' (.y , x'freeMσ≺+xy-y , y'freeσ'y ) | .x , xfreeM , here refl | yes refl = ⊥-elim ((∈-→≢ {xs = fv (M ∙ σ ‚ x := v y)} x'freeMσ≺+xy-y) refl) 
    lemma3← : (y' : 𝒱) → y' *⇂ (σ' ⊙ σ , fv M - x) → y' *⇂ (σ' , fv (M ∙ σ ‚ x := v y) - y)
    lemma3← y' (x' , x'freeM-x , y'freeσσ'x') with lemmafreeσ→ₗ {y'} {σ x'} {σ'} y'freeσσ'x' 
    ... | u , ufreeσx' , y'freeσ'u with lemmafreeσ←ₗ {u} {M} {σ ‚ x := v y} (x' , ∈-→∈ x'freeM-x , lemma)
       where
       lemma : u ∈ fv ((σ ‚ x := v y) x')
       lemma with x ≟ x' 
       ... | yes x≡x' = ⊥-elim (∈-→≢ {xs = fv M} x'freeM-x (sym x≡x'))
       ... | no  _    = ufreeσx' 
    ... | ufreeMσ≺+xy = u , lemma∈-≢ ufreeMσ≺+xy (y≢u ufreeσx') , y'freeσ'u 
       where
       y≢u : {u : 𝒱} → u ∈ fv (σ x') → y ≢ u
       y≢u {u} ufreeσx' with u | ufreeσx' | y ≟ u 
       ... | .y | yfreeσx' | yes refl = ⊥-elim ((Xfresh σ (fv M - x)) x' x'freeM-x yfreeσx') 
       ... | _  | _        | no y≢up  =  y≢up     

  subComp : ∀ {M σ σ'} → M ∙ σ ∙ σ' ≡ M ∙ σ' ⊙ σ
  subComp {c _}            = refl
  subComp {v x}   {σ} {σ'} = refl
  subComp {M · N} {σ} {σ'} = cong₂ _·_ (subComp {M}) (subComp {N}) 
  subComp {λ[ x ∶ A ] M} {σ} {σ'} =
    begin≡
    (((λ[ x ∶ A ] M) ∙ σ) ∙ σ')
    ≡⟨ refl ⟩
    ((λ[ y ∶ A ∙ σ ] (M ∙ (σ ‚ x := v y))) ∙ σ')
    ≡⟨ refl ⟩
    (λ[ y' ∶ (A ∙ σ) ∙ σ' ]((M ∙ (σ ‚ x := v y)) ∙ (σ' ‚ y := v y')))
    ≡⟨ cong₂ (λ[_∶_]_ y') (subComp {A} {σ} {σ'}) (subComp {M} {σ ‚ x := v y} {σ' ‚ y := v y'}) ⟩
    (λ[ y' ∶ A ∙ (σ' ⊙ σ) ](M ∙ ((σ' ‚ y := v y') ⊙ (σ ‚ x := v y))))
    ≡⟨ cong (λ M → λ[ y' ∶ A ∙ (σ' ⊙ σ)] M) (subEqRes {M} {(σ' ‚ y := v y') ⊙ (σ ‚ x := v y)} {(σ' ⊙ σ) ‚ x := v y'} ((∼*ρ , lemmaχσ∘≺+ M (v y') σ σ' x))) ⟩
    (λ[ y' ∶ A ∙ (σ' ⊙ σ) ](M ∙ ((σ' ⊙ σ) ‚ x := v y')))
    ≡⟨ cong (λ z → λ[ z ∶ A ∙ (σ' ⊙ σ)](M ∙ ((σ' ⊙ σ) ‚ x := v z))) (lemma3-1 {x} {M} {σ} {σ'}) ⟩
    (λ[ z ∶ A ∙ (σ' ⊙ σ) ](M ∙ ((σ' ⊙ σ) ‚ x := v z)))
    ≡⟨ refl ⟩
    ((λ[ x ∶ A ] M) ∙ (σ' ⊙ σ))
    ◻
    where 
    y = X (σ , fv M - x)
    y' = X (σ' , fv (M ∙ (σ ‚ x := v y)) - y)
    z = X (σ' ⊙ σ , fv M - x)
  subComp {Π[ x ∶ A ] M} {σ} {σ'} =
    begin≡
    (((Π[ x ∶ A ] M) ∙ σ) ∙ σ')
    ≡⟨ refl ⟩
    ((Π[ y ∶ A ∙ σ ] (M ∙ (σ ‚ x := v y))) ∙ σ')
    ≡⟨ refl ⟩
    (Π[ y' ∶ (A ∙ σ) ∙ σ' ]((M ∙ (σ ‚ x := v y)) ∙ (σ' ‚ y := v y')))
    ≡⟨ cong₂ (Π[_∶_]_ y') (subComp {A} {σ} {σ'}) (subComp {M} {σ ‚ x := v y} {σ' ‚ y := v y'}) ⟩
    (Π[ y' ∶ A ∙ (σ' ⊙ σ) ](M ∙ ((σ' ‚ y := v y') ⊙ (σ ‚ x := v y))))
    ≡⟨ cong (λ M → Π[ y' ∶ A ∙ (σ' ⊙ σ)] M) (subEqRes {M} {(σ' ‚ y := v y') ⊙ (σ ‚ x := v y)} {(σ' ⊙ σ) ‚ x := v y'} ((∼*ρ , lemmaχσ∘≺+ M (v y') σ σ' x))) ⟩
    (Π[ y' ∶ A ∙ (σ' ⊙ σ) ](M ∙ ((σ' ⊙ σ) ‚ x := v y')))
    ≡⟨ cong (λ z → Π[ z ∶ A ∙ (σ' ⊙ σ)](M ∙ ((σ' ⊙ σ) ‚ x := v z))) (lemma3-1 {x} {M} {σ} {σ'}) ⟩
    (Π[ z ∶ A ∙ (σ' ⊙ σ) ](M ∙ ((σ' ⊙ σ) ‚ x := v z)))
    ≡⟨ refl ⟩
    ((Π[ x ∶ A ] M) ∙ (σ' ⊙ σ))
    ◻
    where 
    y = X (σ , fv M - x)
    y' = X (σ' , fv (M ∙ (σ ‚ x := v y)) - y)
    z = X (σ' ⊙ σ , fv M - x)

  composRenUpd : ∀ {x z M N σ} → z ∉ fv M - x → M ∙ (σ ‚ x := N) ≡ M [ x := v z ] ∙ (σ ‚ z := N)
  composRenUpd {x} {z} {M} {N} {σ} z#λxM rewrite subComp {M} {ι ‚ x := v z} {σ ‚ z := N} = subEqRes {M} {σ ‚ x := N} {(σ ‚ z := N) ⊙ (ι ‚ x := v z)} (∼*ρ , lemma)
    where
    lemma : (w : 𝒱) → w ∈ fv M → (σ ‚ x := N) w ≡ (((σ ‚ z := N) ⊙ (ι ‚ x := v z)) w) 
    lemma w wfreeM with x ≟ w
    ... | no x≢w  with z ≟ w
    ... | no _    = refl
    ... | yes z≡w = ⊥-elim ((z≢w x z w M z#λxM wfreeM x≢w) z≡w)
      where
      z≢w : (x z w : 𝒱)(M : Λ) → z ∉ fv M - x → w ∈ fv M → x ≢ w → z ≢ w
      z≢w x z w M z∉fvM-x x*M x≢w with z ≟ x
      z≢w .z z w M _ _ z≢w         | yes refl = z≢w
      z≢w x z w M _ _ x≢w          | no z≢x with z ≟ w
      z≢w x z w M _ _ x≢w          | no z≢x | no z≢w   = z≢w
      z≢w x z .z M z∉fvM-x z*M x≢z | no _   | yes refl = ⊥-elim ((lemma∉-≢ z∉fvM-x (sym≢ x≢z))  z*M)
    lemma w wfreeM | yes _ with z ≟ z 
    ... | yes _   = refl
    ... | no z≢z  = ⊥-elim (z≢z refl)

  corollarylemma≺+ : {x y : 𝒱}{M : Λ} → y ∉ fv M - x → (M ∙ ι ‚ x := v y) ∙ ι ‚ y := v x ≡ M ∙ ι ‚ x := v x
  corollarylemma≺+ {x} {y} {M} y#λxM = sym (composRenUpd {x} {y} {M} y#λxM)

  lemma≺+ι : {x y : 𝒱}{M : Λ} → y ∉ fv M - x → (M ∙ ι ‚ x := v y) ∙ ι ‚ y := v x ≡ M ∙ ι 
  lemma≺+ι {x} {y} {M} y#λxM = begin≡
                                 (M ∙ ι ‚ x := v y) ∙ ι ‚ y := v x
                               ≡⟨ corollarylemma≺+ {x} {y} {M} y#λxM ⟩
                                 M ∙ ι ‚ x := v x
                               ≡⟨ lemmaMι≺+x,x {x} {M} ⟩
                                 M ∙ ι 
                               ◻

  subDistribUpd : ∀ {M N σ x} → M ∙ (σ ‚ x := (N ∙ σ)) ≡ M ∙ (ι ‚ x := N) ∙ σ
  subDistribUpd {M} {N} {σ} {x}
    = begin≡
        M ∙ σ ‚ x := (N ∙ σ)
     ≡⟨ subEqRes {M} (prop6 (lemma≅≺+ {x} {N ∙ σ} (lemmaι {σ}))) ⟩
        M ∙ (σ ⊙ ι) ‚ x := (N ∙ σ)
     ≡⟨ subEqRes {M}  (prop6 {(σ ⊙ ι) ‚ x := (N ∙ σ)} {σ ⊙ ι ‚ x := N} {fv M} (prop7 {x})) ⟩
        M ∙ σ ⊙ ι ‚ x := N
     ≡⟨  sym (subComp {M}) ⟩
        (M ∙ ι ‚ x := N) ∙ σ
      ◻