{-# OPTIONS --termination-depth=3 #-}
module Subst where

open import Ty                                         using (Var; Con; _⇒_; 𝕋; 𝕋s; 𝕋𝕋; 𝕋𝕋s; 𝕍ar; 𝕍ars; _≟t_; vars)
open import Relation.Nullary                           using (Dec; yes; no; ¬_)
open import Data.List                                  using (List; []; {- [_];-} _∷_; _∷ʳ_; map; _++_)
open import Data.Product                               using (_×_; _,_; proj₁; proj₂; ∃; Σ)
open import Data.Maybe.Core                            using (Maybe; nothing; just)
open import Data.Bool                                  using (false)
open import Data.Nat                                   using (ℕ; _≟_)
open import Relation.Nullary                           using (yes; no)
open import Data.Empty                                 using (⊥; ⊥-elim)
open import Data.Unit                                  using (⊤)
open import Data.Sum                                   using (_⊎_; inj₁; inj₂)
open import Function                                   using (case_of_)

open import Relation.Binary                            using (Decidable)
open import Relation.Binary.PropositionalEquality      using (cong;  _≡_; refl; sym; inspect; [_]; Reveal_is_)
open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)
open import Data.Sum                                   using (_⊎_; inj₁; inj₂; [_,_]′)
open import Relation.Nullary.Negation                  using (¬?)
open import Data.List.Any                              using (Any; here; there) 
open Data.List.Any.Membership-≡                        using (_∈_; _⊆_ )

replace : 𝕍ar → 𝕋 → 𝕋 → 𝕋
-- substitute τ for v in τ'. 
replace v τ (Var v') with v ≟ v' 
replace v τ (Var .v) | yes refl = τ
replace v τ (Var v') | no  _ = Var v'
replace v τ (Con c)   = Con c
replace v τ (τ₁ ⇒ τ₂) = replace v τ τ₁ ⇒ replace v τ τ₂

lemRepVar₀ : ∀ (v : 𝕍ar) (τ : 𝕋) → replace v τ (Var v) ≡ τ
lemRepVar₀ v τ with v ≟ v 
lemRepVar₀ v τ | yes refl = refl
lemRepVar₀ v τ | no p     = ⊥-elim (p refl)

-- _≢_ : ∀ {A : Set} → A → A → Set
-- x ≢ y = ¬ x ≡ y

lemRepVar₁ : ∀ {v τ x} → (¬ (v ≡ x)) → replace v τ (Var x) ≡ Var x 
-- Bug? If (¬ (v ≡ x)) is replaced by v ≢ x, error says: ≢ not in scope. Weird.
lemRepVar₁ {v} {τ} {x} p with v ≟ x 
lemRepVar₁ {v} {τ} {x} p | yes p' = ⊥-elim (p p')
lemRepVar₁ {v} {τ} {x} p | no _   = refl

{- lemRepVar∩̸ : ∀ {v τ₀ τ} → ¬ (v ∈ vars τ) → replace v τ₀ τ ≡ τ
lemRepVar∩̸ {v} {τ₀} {Var v'}  v∉vsτ with v ≟ v' 
lemRepVar∩̸ {v} {τ₀} {Var .v}  v∉vsτ | yes refl = ⊥-elim (v∉vsτ (here refl)) 
lemRepVar∩̸ {v} {τ₀} {Var v'}  v∉vsτ | no p = refl
lemRepVar∩̸ {v} {τ₀} {Con _}   v∉vsτ = refl
lemRepVar∩̸ {v} {τ₀} {τ₁ ⇒ τ₂} v∉vsτ = begin
  replace v τ₀ (τ₁ ⇒ τ₂} 
  replace v τ₀ (τ₁ ⇒ τ₂) ≡⟨ refl ⟩

-}

lem∈x⇒∈HdTlx : ∀ { A : Set } {a b : A} {x : List A} → a ∈ (b ∷ x) → (a ≡ b) ⊎ (a ∈ x)
lem∈x⇒∈HdTlx (here a∈b∷x)  = inj₁ a∈b∷x
lem∈x⇒∈HdTlx (there a∈b∷x) = inj₂ a∈b∷x

{- lem_x⊆y_a∈y_a:x⊆y : ∀ {A : Set} {a : A} {x y : List A} → x ⊆ y → a ∈ y → (a ∷ x) ⊆ y
lem_x⊆y_a∈y_a:x⊆y {A} {a} x⊆y a∈y  = λ a∈x → case lem∈x⇒∈HdTlx a∈x of λ
                                               { (inj₁ a∈a) → {!!} -- a∈y -- Weird... bug: if I replace the hole by a∈y,
                                                                          --  an error is detected at the other case (inj₂ a∈bx). 
                                               ; (inj₂ a∈bx) → x⊆y a∈bx 
                                               }
-}

lem_a[] : ∀ {A : Set}  {a : A} → ¬ (a ∈ []) 
lem_a[] {A} {a} = λ ()

lem∉⇒∉∷ : ∀ {A : Set} (a b : A) (x : List A) → ¬ (a ∈ x) → ¬ (a ≡ b) → ¬ (a ∈ (b ∷ x))
lem∉⇒∉∷ a b x a∉x a≢b = λ x → case lem∈x⇒∈HdTlx x of λ 
                                { (inj₁ a≡b) → a≢b a≡b
                                ; (inj₂ a∈x) → a∉x a∈x
                                }

elem⊆ : ∀ {A : Set} (a : A) (x y : List A) → x ⊆ y → (a ∈ x) → (a ∈ y)
elem⊆ a x y x⊆y a∈x = x⊆y a∈x

notElem⊆ : ∀ {A : Set} (a : A) (x y : List A) → x ⊆ y → ¬ (a ∈ y) → ¬ (a ∈ x)
notElem⊆ a x y x⊆y a∉y  = λ a∈x → a∉y (x⊆y a∈x)
 
lemx≡x++[] : ∀ {A : Set} {x : List A} → x ≡ (x ++ [])
lemx≡x++[] {A} {[]}    = refl
lemx≡x++[] {A} {b ∷ x} = cong (_∷_ b) lemx≡x++[]

lem∈xy⇒∈xOr∈y : ∀ {A : Set} {a : A} (x y : List A) → a ∈ (x ++ y) → (a ∈ x) ⊎ (a ∈ y)
lem∈xy⇒∈xOr∈y [] (b ∷ y) (here a∈y)   = inj₂ (here a∈y) 
lem∈xy⇒∈xOr∈y [] (b ∷ y) (there a∈y)  = inj₂ (there a∈y)
lem∈xy⇒∈xOr∈y (b ∷ x) []  (here a∈bx)  = inj₁ (here a∈bx)
lem∈xy⇒∈xOr∈y (b ∷ x) []  (there a∈bx) with lem∈xy⇒∈xOr∈y x [] a∈bx
lem∈xy⇒∈xOr∈y (b ∷ x) []  (there a∈bx) | (inj₁ a∈x) = inj₁ (there a∈x)
lem∈xy⇒∈xOr∈y (b ∷ x) []  (there a∈bx) | (inj₂ a∈[]) = ⊥-elim (lem_a[] a∈[])
lem∈xy⇒∈xOr∈y (b ∷ x) (c ∷ y) (here a∈bx)  = inj₁ (here a∈bx)
lem∈xy⇒∈xOr∈y (b ∷ x) (c ∷ y) (there a∈xcy) with lem∈xy⇒∈xOr∈y x (c ∷ y) a∈xcy 
lem∈xy⇒∈xOr∈y (b ∷ x) (c ∷ y) (there a∈xcy) | (inj₁ inxcy) = inj₁ (there inxcy)
lem∈xy⇒∈xOr∈y (b ∷ x) (c ∷ y) (there a∈xcy) | (inj₂ incy)  = inj₂ incy 
lem∈xy⇒∈xOr∈y [] []  () 

lem∉⇒∉++ : ∀ {A : Set} {a : A} {x y : List A} → ¬ (a ∈ x) → ¬ (a ∈ y) → ¬ (a ∈ (x ++ y))
lem∉⇒∉++ {A} {a} {x} {y} a∉x a∉y = λ x' → case lem∈xy⇒∈xOr∈y x y x' of λ 
                                                 { (inj₁ a∈x) → a∉x a∈x
                                                 ; (inj₂ a∈y) → a∉y a∈y
                                                 }

lem∈⇒∈++ : ∀ {A : Set} {a : A} {x y : List A} → a ∈ x → a ∈ (x ++ y)
lem∈⇒∈++ (here px) = here px
lem∈⇒∈++ (there p) = there (lem∈⇒∈++ p) 

lem∉both⇒∈++ : ∀ {A : Set} {a : A} {x y : List A} → (¬ (a ∈ x)) × (¬ (a ∈ y)) → ¬ (a ∈ (x ++ y))
lem∉both⇒∈++ {A} {a} {x} {y} (a∉x , a∉y) = λ a∈xy → case lem∈xy⇒∈xOr∈y {A} {a} x y a∈xy of λ 
                                                      { (inj₁ inx) → a∉x inx
                                                      ; (inj₂ iny) → a∉y iny
                                                      }

lem∈⇒∈++' : ∀ {A : Set} {a : A} {x y : List A} → a ∈ y → a ∈ (x ++ y)
lem∈⇒∈++' {A} {a} {[]} a∈x = a∈x
lem∈⇒∈++' {A} {a} {x ∷ xs} {y} a∈xy = there (lem∈⇒∈++' {A} {a} {xs} {y} a∈xy)

lem∉++⇒∉ : ∀ {A : Set} {a : A} {x y : List A} → ¬ (a ∈ x ++ y) → (¬ (a ∈ x) × ¬ (a ∈ y))
lem∉++⇒∉ {A} {a} {x} {y} a∈xy = (λ a∈x → a∈xy (lem∈⇒∈++ a∈x)) , (λ a∈y → a∈xy (lem∈⇒∈++' {A} {a} {x} {y} a∈y))

Dom : Set
Dom = 𝕍ars

Rng : Set
Rng = 𝕍ars

_∩̸_ : {A : Set} (x y : List A) → Set _ 
x ∩̸ y = ∀ {a} → a ∈ x → (¬ (a ∈ y))

data Subs : Dom → Rng → Set where
  emptySubs : ∀ {rng} → Subs [] rng
  mkSubs    : ∀ {v τ dom rng} → vars τ ⊆ rng → Subs dom rng → 
                 ( (¬ (v ∈ dom)) × (¬ (v ∈ rng)) × (dom ∩̸ rng)) → Subs (v ∷ dom) rng

apply : ∀ {dom rng} → Subs dom rng → 𝕋 → 𝕋 
apply emptySubs                       τ = τ 
apply (mkSubs {v} {τ₀} {_} {_} _ s _) τ = apply s (replace v τ₀ τ)

head∈ : ∀ {A : Set} {v : A} {vs : List A} → v ∈ (v ∷ vs)
head∈ {v} {vs} = here refl

filterNotOccs : ∀ (vs₁ vs₂ vs : 𝕍ars) → vs₂ ⊆ vs → vs₁ ∩̸ vs → vs₁ ∩̸ vs₂
filterNotOccs []         _           _ vs₂⊆vs vs₁∩̸vs = λ z z' → vs₁∩̸vs z (vs₂⊆vs z') 
filterNotOccs (v₁ ∷ vs₁) []          _ []⊆vs  vs₁∩̸vs = λ z z' → vs₁∩̸vs z ([]⊆vs z')
filterNotOccs (v₁ ∷ vs₁) (v₂ ∷ vs₂') _ vs₂⊆vs vs₁∩̸vs = λ z z' → vs₁∩̸vs z (vs₂⊆vs z')

lemVars++ : ∀ {τ₁ τ₂} → vars (τ₁ ⇒ τ₂) ≡ vars τ₁ ++ vars τ₂  
lemVars++ {τ₁} {τ₂} = refl

lemOccsFun : ∀ {v : 𝕍ar} {τ₁ τ₂ : 𝕋} → (v ∈ vars (τ₁ ⇒ τ₂)) → (v ∈ vars τ₁) ⊎ (v ∈ vars τ₂)
lemOccsFun {v} {τ₁} {τ₂} v∈varsτ₁⇒τ₂ = lem∈xy⇒∈xOr∈y {ℕ} {v} x y v∈varsτ₁⇒τ₂
  where x = vars τ₁
        y = vars τ₂

lemOccsFun0 : ∀ {v : 𝕍ar} {τ₁ τ₂ : 𝕋} → (v ∈ vars (τ₁ ⇒ τ₂)) → ¬ (v ∈ vars τ₁) → (v ∈ vars τ₂)
lemOccsFun0 {v} {τ₁} {τ₂} v∈τ₁⇒τ₂ v∉τ₁ with lemOccsFun {v} {τ₁} {τ₂} v∈τ₁⇒τ₂
lemOccsFun0 {v} {τ₁} {τ₂} v∈τ₁⇒τ₂ v∉τ₁ | inj₁ v∈τ₁ = ⊥-elim (v∉τ₁ v∈τ₁) 
lemOccsFun0 {v} {τ₁} {τ₂} v∈τ₁⇒τ₂ v∉τ₁ | inj₂ v∈τ₂ = v∈τ₂

lemOcc0 : ∀ {v v'} → (v ≡ v') → (v ∈ vars (Var v'))
lemOcc0 v≡v' = here v≡v'

lemOcc1 : ∀ {v v'} → (v ∈ vars (Var v')) → (v ≡ v')
lemOcc1 (here v≡v')  = v≡v' 
lemOcc1 (there v∈[]) = ⊥-elim (lem_a[] v∈[])

lemNotOcc0 : ∀ {v v'} → ¬ (v ≡ v') → ¬ (v ∈ vars (Var v'))
lemNotOcc0 {v} {v'} v≢v' with v ≟ v'
lemNotOcc0 {v} {.v} v≢v' | yes refl = λ _ → v≢v' refl
lemNotOcc0 {v} {v'} v≢v' | no p = λ v∈Varv' → v≢v' (lemOcc1 v∈Varv')

lemNotOccsFun : ∀ {v τ₁ τ₂} → ¬ (v ∈ vars (τ₁ ⇒ τ₂)) → ¬ (v ∈ vars τ₁) × ¬ (v ∈ vars τ₂)
lemNotOccsFun {v} {τ₁} {τ₂} v∉τ₁⇒τ₂ = (proj₁ p , proj₂ p)
  where p : ¬ (v ∈ vars τ₁) × ¬ (v ∈ vars τ₂)
        p = lem∉++⇒∉ v∉τ₁⇒τ₂

lemNotOccs⇒NotElem : ∀ {A : Set} {a : A} {x y : List A} → x ∩̸ y → a ∈ x → ¬ (a ∈ y)
lemNotOccs⇒NotElem {a} {x} {y} x∩̸y a∈x = x∩̸y a∈x

lemNotOccVs : ∀ {A : Set} {y z x x' : List A} → y ⊆ z → x ∩̸ z → x' ⊆ x → y ∩̸ x'
lemNotOccVs y⊆z x∩̸z x'⊆x a∈y a∈x' = x∩̸z (x'⊆x a∈x') (y⊆z a∈y) 

∩̸Tail : ∀ {A : Set} {a : A} {x y : List A} → (a ∷ x) ∩̸ y → x ∩̸ y
∩̸Tail ax∩̸y (here p) = ax∩̸y (there (here p))
∩̸Tail ax∩̸y (there p) = ∩̸Tail (λ z → ax∩̸y (there z)) p

lemNotElem : ∀ {A : Set} {a : A} {x y : List A} → ¬ (a ∈ x) → y ⊆ x → ¬ (a ∈ y)
lemNotElem {A} {a} {x} {y} a∉x y⊆x a∈y = a∉x (y⊆x a∈y)

lemNotElem' : ∀ {A : Set} {a : A} {x y : List A} → (a ∷ y) ∩̸ x → ¬ (a ∈ x)
lemNotElem' {A} {a} {x} {y} ay∩̸x a∈x = ay∩̸x (here refl) a∈x 


∩̸∷ : ∀ {A : Set} {a : A} {x y : List A} → ¬ (a ∈ y) → x ∩̸ y → (a ∷ x) ∩̸ y
∩̸∷ a∉y x∩̸y (here refl) = λ x → a∉y x
∩̸∷ a∉y x∩̸y (there a₁∈a:x) = x∩̸y a₁∈a:x

∩̸++ : ∀ {A : Set} {x₁ x₂ y : List A} → x₁ ∩̸ y → x₂ ∩̸ y → (x₁ ++ x₂) ∩̸ y
∩̸++ {_} {x₁} {x₂} x₁∩̸y x₂∩̸y a∈x₁x₂ y = case lem∈xy⇒∈xOr∈y x₁ x₂ a∈x₁x₂ of λ 
                                                   { (inj₁ inx₁) → x₁∩̸y inx₁ y 
                                                   ; (inj₂ inx₂) → x₂∩̸y inx₂ y 
                                                   }

∩̸[] : ∀ {A : Set} {x : List A} → x ∩̸ [] 
∩̸[] = λ _ → lem_a[] 

∩̸[]' : ∀ {A : Set} {x : List A} → [] ∩̸ x
∩̸[]' = λ ()

ax⊆x : ∀ {a : ℕ} {x : List ℕ} → x ⊆ (a ∷ x)
ax⊆x {a} {x} = there

x⊆x : ∀ {x : List ℕ} → x ⊆ x
x⊆x {x} = λ x → x

lemRepNotElem : ∀ {v τ} → (τ₀ : 𝕋) → (¬ (v ∈ vars τ)) → (replace v τ₀ τ ≡ τ)
lemRepNotElem {v} {Var v'}  τ₀ v∉varsτ with v ≟ v'
lemRepNotElem {v} {Var .v}  τ₀ v∉varsτ | yes refl = ⊥-elim (v∉varsτ (here refl))
lemRepNotElem {v} {Var v'}  τ₀ v∉varsτ | no p = refl 
lemRepNotElem {v} {Con c}   τ₀ v∉varsτ = refl
lemRepNotElem {v} {τ₁ ⇒ τ₂} τ₀ v∉varsτ = begin
  replace v τ₀ (τ₁ ⇒ τ₂) ≡⟨ refl ⟩
  replace v τ₀ τ₁ ⇒ replace v τ₀ τ₂ ≡⟨ cong (λ τ → τ ⇒ replace v τ₀ τ₂) (lemRepNotElem τ₀ (proj₁ (lemNotOccsFun {v} {τ₁} {τ₂} v∉varsτ))) ⟩
  τ₁ ⇒ replace v τ₀ τ₂ ≡⟨ cong (λ τ → τ₁ ⇒ τ) (lemRepNotElem τ₀ (proj₂ (lemNotOccsFun {v} {τ₁} {τ₂} v∉varsτ))) ⟩
  τ₁ ⇒ τ₂ ∎


lemAppCon : ∀ {dom} {rng} {s : Subs dom rng} {c} → apply s (Con c) ≡ Con c
lemAppCon {[]} {_} {emptySubs} {c} = refl
lemAppCon {v ∷ dom} {rng} {mkSubs {.v} {τ₀} {.dom} {.rng} varsτ₀⊆rng s' noInter} {c} = begin
  apply (mkSubs {v} {τ₀} {dom} {rng} varsτ₀⊆rng s' noInter) (Con c) ≡⟨ refl ⟩
  apply s' (Con c)                                                  ≡⟨ lemAppCon {dom} {rng} {s'} {c} ⟩
  Con c ∎
 
lemAppEmptyDom : ∀ {rng τ} → (s : Subs [] rng) → apply s τ ≡ τ
lemAppEmptyDom emptySubs = refl

lemAppNotOccDom : ∀ {dom} {rng} {s : Subs dom rng} → (τ : 𝕋) → (vars τ) ∩̸ dom → apply s τ ≡ τ
lemAppNotOccDom {dom} {rng} {s} (Con c) _ = lemAppCon {dom} {rng} {s} {c}
lemAppNotOccDom {[]} {_} {s} (Var _) _    = lemAppEmptyDom s
lemAppNotOccDom {v' ∷ dom'} {rng} {mkSubs {.v'} {τ'} {.dom'} {.rng} v'∉rng s' noInterrng} (Var v) noIntervarsτdom  = 
 begin
  apply (mkSubs {v'} {τ'} {dom'} {rng} v'∉rng s' noInterrng) (Var v) ≡⟨ refl ⟩
  apply s' (replace v' τ' (Var v)) ≡⟨ cong (λ τ → apply s' τ) (lemRepVar₁ (λ z → noIntervarsτdom (here z) (here refl))) ⟩
  apply s' (Var v) ≡⟨ lemAppNotOccDom {dom'} {rng} {s'} (Var v) (λ {v0} z z' → noIntervarsτdom z (there z')) ⟩
  Var v 
 ∎
lemAppNotOccDom {[]} {rng} {emptySubs} (τ₁ ⇒ τ₂) _ = refl
lemAppNotOccDom {v' ∷ dom'} {rng} {mkSubs {.v'} {τ'} {.dom'} {.rng} v'∉rng s' noInter} (τ₁ ⇒ τ₂) noInter' = 
 begin
  apply (mkSubs {v'} {τ'} {dom'} {rng} v'∉rng s' noInter) (τ₁ ⇒ τ₂) ≡⟨ refl ⟩
  apply s' (replace v' τ' (τ₁ ⇒ τ₂)) ≡⟨ cong (λ τ → apply s' τ) (lemRepNotElem {v'} {τ₁ ⇒ τ₂} τ' (λ z → noInter' z (here refl))) ⟩
  apply s' (τ₁ ⇒ τ₂) ≡⟨ lemAppNotOccDom {dom'} {rng} {s'} (τ₁ ⇒ τ₂) (λ {v} z z' → noInter' z (there z')) ⟩
  τ₁ ⇒ τ₂ 
 ∎

lemAppFun : ∀ {dom} {rng} {s : Subs dom rng} {τ₁} {τ₂} → (apply s (τ₁ ⇒ τ₂) ≡ (apply s τ₁ ⇒ apply s τ₂))
lemAppFun {[]} {_} {emptySubs} {_} {_} = refl
lemAppFun {v ∷ dom} {rng} {mkSubs {.v} {τ} {.dom} {.rng} varsτ⊆rng s' noInter} {τ₁} {τ₂} = 
  begin 
    apply (mkSubs {v} {τ} {dom} {rng} varsτ⊆rng s' noInter) (τ₁ ⇒ τ₂) ≡⟨ refl ⟩
    apply s' (replace v τ (τ₁ ⇒ τ₂)) ≡⟨ refl  ⟩
    apply s' (replace v τ τ₁ ⇒ replace v τ τ₂) ≡⟨ lemAppFun {dom} {rng} {s'} {replace v τ τ₁} {replace v τ τ₂} ⟩
    apply s' (replace v τ τ₁) ⇒ apply s' (replace v τ τ₂) ≡⟨ refl ⟩
    apply (mkSubs {v} {τ} {dom} {rng} varsτ⊆rng s' noInter) τ₁ ⇒ apply (mkSubs {v} {τ} {dom} {rng} varsτ⊆rng s' noInter) τ₂ 
  ∎

idempotent : ∀ dom rng (s : Subs dom rng) (τ : 𝕋) → apply s (apply s τ) ≡ apply s τ
idempotent dom rng s (Con c) = 
  begin
    apply s (apply s (Con c))  ≡⟨ cong (λ τ → apply s τ) (lemAppCon {dom} {rng} {s} {c}) ⟩
    apply s (Con c) 
  ∎
idempotent [] rng emptySubs (Var v) = refl
idempotent (v ∷ dom) rng (mkSubs {.v} {τ₀} {.dom} {.rng} vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (Var v') with v ≟ v' | inspect (_≟_ v v')
idempotent (v ∷ dom) rng (mkSubs {.v} {τ₀} {.dom} {.rng} vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (Var .v) | yes refl  | [ (yes refl) ] = 
  begin
   apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (Var v)) 
      ≡⟨ refl ⟩
   apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (apply s' (replace v τ₀ (Var v)))
      ≡⟨ cong (λ τ → apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (apply s' τ)) (lemRepVar₀ v τ₀) ⟩ 
   apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (apply s' τ₀) 
      ≡⟨ cong (λ τ → apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) τ) (lemAppNotOccDom τ₀ (lemNotOccVs vsτ₀⊆rng dom∩̸rng x⊆x)) ⟩
-- lemNotOccVs : ∀ {A : Set} {y z x x' : List A} → y ⊆ z → x ∩̸ z → x' ⊆ x → y ∩̸ x'
-- lemAppNotOccDom : ∀ {dom} {rng} {s : Subs dom rng} → (τ : 𝕋) → (vars τ) ∩̸ dom → apply s τ ≡ τ
-- lemRepNotElem : ∀ {v τ} → (τ₀ : 𝕋) → (¬ (v ∈ vars τ)) → (replace v τ₀ τ ≡ τ)
-- ∩̸∷ : ∀ {A : Set} {a : A} {x y : List A} → ¬ (a ∈ y) → x ∩̸ y → (a ∷ x) ∩̸ y
-- lemNotElem : ∀ {A : Set} {a : A} {x y : List A} → ¬ (a ∈ x) → y ⊆ x → ¬ (a ∈ y)
   apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) τ₀ 
      ≡⟨ sym refl ⟩ -- (lemAppNotOccDom τ₀ (lemNotOccVs vsτ₀⊆rng (∩̸∷ v∉dom dom∩̸rng) x⊆x))
   apply s' (replace v τ₀ τ₀)
      ≡⟨ cong (λ τ → apply s' τ) (lemRepNotElem {v} {τ₀} τ₀ (lemNotElem {ℕ} {v} {rng} {vars τ₀} v∉rng vsτ₀⊆rng)) ⟩
   apply s' τ₀
      ≡⟨ sym (cong (λ τ → apply s' τ) (lemRepVar₀ v τ₀)) ⟩
   apply s' (replace v τ₀ (Var v)) 
      ≡⟨ sym refl ⟩
   apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (Var v)
  ∎
idempotent (v ∷ dom) rng (mkSubs {.v} {τ₀} {.dom} {.rng} vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (Var v') | (no p) | _ = {!!}
-- -- apply (mkSubs {v} {τ₀} {_} {_} _ s _) τ = apply s (replace v τ₀ τ)
{-
    rewrite (lemRepVar₁ p) = 
 begin
  apply (mkSubs {v} {τ₀} {dom} {rng} vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) 
        (apply (mkSubs {v} {τ₀} {dom} {rng} vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (Var v'))
     ≡⟨ refl ⟩
  apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (apply s' (replace v τ₀ (Var v')))
     ≡⟨ cong (λ τ → apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (apply s' τ)) (lemRepVar₁ {v} {τ₀} {v'} p) ⟩ 
  apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (apply s' (Var v'))
     ≡⟨ refl ⟩ 
  apply s' (replace v τ₀ (apply s' (Var v')))
     ≡⟨ cong (λ τ → apply s' (replace v τ₀ τ)) (lemRepNotElem τ₀ (lemNotElem v∉rng vsτ₀⊆rng)) ⟩ 
-- lemRepNotElem : ∀ {v τ} → (τ₀ : 𝕋) → (¬ (v ∈ vars τ)) → (replace v τ₀ τ ≡ τ)
-- lemNotElem : ∀ {A : Set} {a : A} {x y : List A} → ¬ (a ∈ x) → y ⊆ x → ¬ (a ∈ y)
  apply s' (apply s' (Var v')) 
     ≡⟨ idempotent dom rng s' (Var v') ⟩
  apply s' (Var v')
     ≡⟨ cong (λ τ → apply s' τ) (sym (lemRepVar₁ {v} {τ₀} {v'} p) ) ⟩
  apply s' (replace v τ₀ (Var v')) 
     ≡⟨ sym refl ⟩
  apply (mkSubs {v} {τ₀} {dom} {rng} vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (Var v')
 ∎
-}
idempotent dom rng s (τ₁ ⇒ τ₂) = 
 begin
   apply s (apply s (τ₁ ⇒ τ₂))                 ≡⟨ cong (λ τ → apply s τ) (lemAppFun {dom} {rng} {s} {τ₁} {τ₂}) ⟩
   apply s (apply s τ₁ ⇒ apply s τ₂)           ≡⟨ lemAppFun {dom} {rng} {s} {apply s τ₁} {apply s τ₂} ⟩
   apply s (apply s τ₁) ⇒ apply s (apply s τ₂) ≡⟨ cong (λ τ → apply s (apply s τ₁) ⇒ τ) (idempotent dom rng s τ₂) ⟩ 
   apply s (apply s τ₁) ⇒ apply s τ₂           ≡⟨ cong (λ τ → τ ⇒ apply s τ₂) (idempotent dom rng s τ₁) ⟩ 
   apply s τ₁ ⇒ apply s τ₂                     ≡⟨ sym (lemAppFun {dom} {rng} {s} {τ₁} {τ₂}) ⟩ 
   apply s (τ₁ ⇒ τ₂) 
 ∎
--------------------------------------------------------------------------------------------------------------
compose : ∀ { x₁ x₂ y } → Subs x₁ y → x₁ ∩̸ x₂ → Subs x₂ y → Subs (x₁ ++ x₂) y
compose emptySubs _ s = s
compose (mkSubs {v} {τ} {x₁} {y} vsτ₀⊆y s₁ (v∉x₁ , v∉y , x₁∩̸y)) vx₁∩̸x₂ emptySubs = 
  mkSubs {v} {τ} {x₁ ++ []} {y} vsτ₀⊆y (compose s₁ (∩̸[] {_} {x₁}) emptySubs) 
                (                      lem∉⇒∉++ v∉x₁ lem_a[] , v∉y , ∩̸++ {_} {x₁} {[]} x₁∩̸y ∩̸[]')
compose (mkSubs {v₁} {τ₁} {x₁} {y} vsτ₁⊆y s₁ (v₁∉x₁ , v₁∉y , x₁∩̸y)) v₁x₁∩̸v₂x₂ 
        (mkSubs {v₂} {τ₂} {x₂} {.y} vsτ₂⊆y s₂ (v₂∉x₂ , v₂∉y , x₂∩̸y)) =  
  mkSubs {v₁} {τ₁} {x₁ ++ (v₂ ∷ x₂)} {y} vsτ₁⊆y (compose s₁ (∩̸Tail v₁x₁∩̸v₂x₂) 
                                                 (mkSubs {v₂} {τ₂} {x₂} {y} vsτ₂⊆y s₂ (v₂∉x₂ , v₂∉y , x₂∩̸y)))
                                  (lem∉⇒∉++ v₁∉x₁ (lemNotElem' v₁x₁∩̸v₂x₂) , v₁∉y , ∩̸++ x₁∩̸y (∩̸∷ v₂∉y x₂∩̸y))

--------------------------------------------------------------------------------------------------------------