Stoughton.Alpha

open import Stoughton.Var

module Stoughton.Alpha (𝒞 : 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 𝒞 𝒱 _≟_
  open import Stoughton.Substitution 𝒞 var 
  open import Stoughton.Renaming 𝒞 var
  
  open import Function
  open import Data.Empty
  open import Relation.Nullary
  open import Data.List hiding (length)
  open import Data.Nat hiding (_*_; _≟_)
  open import Data.Nat.Properties hiding (_≟_)
  open import Data.Product renaming (Σ to Σₓ) hiding (map)
  open import Data.List.Relation.Unary.Any hiding (map)
  open import Data.List.Membership.Propositional
  open import Data.List.Membership.Propositional.Properties  
  open import Data.List.Properties
  open import Relation.Binary
  open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; _≢_; refl; sym; cong; cong₂; trans; subst)
  open PropEq.≡-Reasoning 

  infix  3 _∼α_ 
  data _∼α_ : Λ → Λ → Set where
    ∼c : ∀ {k} → c k ∼α c k
    ∼v : ∀ {x} → v x ∼α v x
    ∼· : ∀ {M M' N N'} → M ∼α M' → N ∼α N' → M · N ∼α M' · N'
    ∼λ : ∀ {x x' y A A' M M'} → A ∼α A' → y ∉ fv M - x → y ∉ fv M' - x' → M [ x := v y ] ≡ M' [ x' := v y ] → λ[ x ∶ A ] M ∼α λ[ x' ∶ A' ] M'
    ∼Π : ∀ {x x' y A A' B B'} → A ∼α A' → y ∉ fv B - x → y ∉ fv B' - x' → B [ x := v y ] ≡ B' [ x' := v y ] → Π[ x ∶ A ] B ∼α Π[ x' ∶ A' ] B' 

  iotaAlpha : {M M' : Λ} → M ∙ ι ≡ M' ∙ ι → M ∼α M' 
  iotaAlpha {c x}   {c .x}   refl = ∼c
  iotaAlpha {c x}   {v y}     ()
  iotaAlpha {c x}   {M · N}   ()
  iotaAlpha {c x}   {λ[ _ ∶ _ ] _}  ()
  iotaAlpha {v x}   {c k}     () 
  iotaAlpha {v x}   {v .x}    refl = ∼v
  iotaAlpha {v x}   {M · N}   () 
  iotaAlpha {v x}   {λ[ _ ∶ _ ] _}  ()
  iotaAlpha {M · N} {c x}        ()
  iotaAlpha {M · N} {v x}      ()
  iotaAlpha {M · N} {M' · N'} MNι≡M'N'ι = ∼· (iotaAlpha (proj₁ (aux MNι≡M'N'ι))) (iotaAlpha (proj₂ (aux MNι≡M'N'ι)))
    where 
    aux : (M · N) ∙ ι ≡ (M' · N') ∙ ι → M ∙ ι ≡ M' ∙ ι × N ∙ ι ≡ N' ∙ ι
    aux MNι≡M'N'ι with M' ∙ ι | N' ∙ ι | MNι≡M'N'ι
    ... | .(M ∙ ι) | .(N ∙ ι) | refl = refl , refl
  iotaAlpha {M · N} {λ[ _ ∶ _ ] _}     ()
  iotaAlpha {λ[ _ ∶ _ ] _} {c _}        () 
  iotaAlpha {λ[ _ ∶ _ ] _} {v y}        () 
  iotaAlpha {λ[ _ ∶ _ ] _} {M' · N'}    ()
  iotaAlpha {λ[ x ∶ A ] M} {λ[ x' ∶ A' ] M'} λxMι≡λx'M' with aux λxMι≡λx'M' 
    where
    aux : λ[ x ∶ A ] M ∙ ι ≡ λ[ x' ∶ A' ] M' ∙ ι → X (ι , fv M - x) ≡ X (ι , fv M' - x') × M ∙ ι ‚ x := v (X (ι , fv M - x)) ≡ M' ∙ ι ‚ x' := v (X (ι , fv M' - x')) × A ∙ ι ≡ A' ∙ ι
    aux λxMι#λx'M'ι with A ∙ ι | X (ι , fv M - x) | M ∙ ι ‚ x := v (X (ι , fv M - x)) | λxMι#λx'M'ι 
    ... | .(A' ∙ ι) | .(X (ι , fv M' - x')) | .(M' ∙ ι ‚ x' := v (X (ι , fv M' - x'))) | refl = refl , refl , refl
  ... | y≡y' , Mι≺+xy≡M'ι≺+xy' , Aι=A'ι with X (ι , fv M - x) | X (ι , fv M' - x') | lemma-χιₗ (fv M - x) | lemma-χιₗ (fv M' - x') | y≡y' 
  ... | y | .y | y#λxM | y#λx'M' | refl = ∼λ {x} {x'} {y} {A} {A'} {M} {M'} A∼A' y#λxM y#λx'M' Mι≺+xy≡M'ι≺+xy'
    where    
    A∼A' : A ∼α A'
    A∼A' = iotaAlpha Aι=A'ι
  iotaAlpha {Π[ x ∶ A ] M} {Π[ x' ∶ A' ] M'} ΠxMι≡Πx'M' with aux ΠxMι≡Πx'M' 
    where
    aux : Π[ x ∶ A ] M ∙ ι ≡ Π[ x' ∶ A' ] M' ∙ ι → X (ι , fv M - x) ≡ X (ι , fv M' - x') × M ∙ ι ‚ x := v (X (ι , fv M - x)) ≡ M' ∙ ι ‚ x' := v (X (ι , fv M' - x')) × A ∙ ι ≡ A' ∙ ι
    aux ΠxMι#Πx'M'ι with A ∙ ι | X (ι , fv M - x) | M ∙ ι ‚ x := v (X (ι , fv M - x)) | ΠxMι#Πx'M'ι 
    ... | .(A' ∙ ι) | .(X (ι , fv M' - x')) | .(M' ∙ ι ‚ x' := v (X (ι , fv M' - x'))) | refl = refl , refl , refl
  ... | y≡y' , Mι≺+xy≡M'ι≺+xy' , Aι=A'ι with X (ι , fv M - x) | X (ι , fv M' - x') | lemma-χιₗ (fv M - x) | lemma-χιₗ (fv M' - x') | y≡y' 
  ... | y | .y | y#ΠxM | y#Πx'M' | refl = ∼Π {x} {x'} {y} {A} {A'} {M} {M'} A∼A' y#ΠxM y#Πx'M' Mι≺+xy≡M'ι≺+xy'
    where    
    A∼A' : A ∼α A'
    A∼A' = iotaAlpha Aι=A'ι

  ∼ρ : Reflexive _∼α_
  ∼ρ {M} = iotaAlpha refl

  ≡⇒∼ : ∀ {M N} → M ≡ N → M ∼α N
  ≡⇒∼ {M} {.M} refl = ∼ρ

  infix  3 _∼αₛ_ 
  data _∼αₛ_ : Λ → Λ → Set where
    ∼c : ∀ {k} → c k ∼αₛ c k
    ∼v : ∀ {x} → v x ∼αₛ v x
    ∼· : ∀ {M M' N N'} → M ∼αₛ M' → N ∼αₛ N' → M · N ∼αₛ M' · N'
    ∼λ : ∀ {M M' x x' y A A'} → A ∼αₛ A' → y ∉ fv M - x → y ∉ fv M' - x' → [ v y / x ] M ∼αₛ [ v y / x' ] M' → λ[ x ∶ A ] M ∼αₛ λ[ x' ∶ A' ] M'
    ∼Π : ∀ {B B' x x' y A A'} → A ∼αₛ A' → y ∉ fv B - x → y ∉ fv B' - x' → [ v y / x ] B ∼αₛ [ v y / x' ] B' → Π[ x ∶ A ] B ∼αₛ Π[ x' ∶ A' ] B' 

  infixl 8 _≺+_
  _≺+_ : Sub → 𝒱 × Λ → Sub
  σ ≺+ (x , N) = σ ‚ x := N

  open import Data.Nat.Induction
  
  iotaAlphaSt-aux : (n : ℕ) → ((y : ℕ) → suc y ≤′ n → (M M' : Λ) → y ≡ length M → M ∙ ι ≡ M' ∙ ι → M ∼αₛ M') → (M M' : Λ) → n ≡ length M → M ∙ ι ≡ M' ∙ ι → M ∼αₛ M'
  iotaAlphaSt-aux .(suc zero) rec (c x)   (c .x)    refl refl = ∼c
  iotaAlphaSt-aux .(suc zero) rec (c x)   (v y)     refl ()
  iotaAlphaSt-aux .(suc zero) rec (c x)   (M · N)   refl ()
  iotaAlphaSt-aux .(suc zero) rec (c x)   (λ[ _ ∶ _ ] _)   refl ()
  iotaAlphaSt-aux .(suc zero) rec (v x)   (c k)     refl () 
  iotaAlphaSt-aux .(suc zero) rec (v x)   (v .x)    refl refl = ∼v
  iotaAlphaSt-aux .(suc zero) rec (v x)   (M · N)   refl () 
  iotaAlphaSt-aux .(suc zero) rec (v x)   (λ[ _ ∶ _ ] _)   refl ()
  iotaAlphaSt-aux n           rec (M · N) (c x)     _    ()
  iotaAlphaSt-aux n           rec (M · N) (v x)     _    ()
  iotaAlphaSt-aux .(suc (length M + length N)) rec (M · N) (M' · N') refl MNι≡M'N'ι
    = ∼· (rec (length M) (s≤′s (m≤′m+n (length M) (length N))) M M' refl (proj₁ (lemmaMι≡M'ι MNι≡M'N'ι)))
         (rec (length N) (s≤′s (n≤′m+n (length M) (length N))) N N' refl (proj₂ (lemmaMι≡M'ι MNι≡M'N'ι)))
    where 
    lemmaMι≡M'ι : (M · N) ∙ ι ≡ (M' · N') ∙ ι → M ∙ ι ≡ M' ∙ ι × N ∙ ι ≡ N' ∙ ι
    lemmaMι≡M'ι MNι≡M'N'ι with M' ∙ ι | N' ∙ ι | MNι≡M'N'ι
    ... | .(M ∙ ι) | .(N ∙ ι) | refl = refl , refl
  iotaAlphaSt-aux n           rec (M · N) (λ[ _ ∶ _ ] _)  _    ()
  iotaAlphaSt-aux n           rec (λ[ _ ∶ _ ] _) (c _)     _    () 
  iotaAlphaSt-aux n           rec (λ[ _ ∶ _ ] _) (v y)     _    () 
  iotaAlphaSt-aux n           rec (λ[ _ ∶ _ ] _) (M' · N') _    ()
  iotaAlphaSt-aux .(suc (length A + length M)) rec (λ[ x ∶ A ] M) (λ[ x' ∶ A' ] M') refl λxMι≡λx'M' with λxMι≡λx'M'ι λxMι≡λx'M' 
    where
    λxMι≡λx'M'ι : λ[ x ∶ A ] M ∙ ι ≡ λ[ x' ∶ A' ] M' ∙ ι → X (ι , fv M - x) ≡ X (ι , fv M' - x') × M ∙ ι ≺+ (x , v (X (ι , fv M - x))) ≡ M' ∙ ι ≺+ (x' , v (X (ι , fv M' - x'))) × A ∙ ι ≡ A' ∙ ι
    λxMι≡λx'M'ι λxMι#λx'M'ι with A ∙ ι | X (ι , fv M - x) | M ∙ ι ≺+ (x , v (X (ι , fv M - x))) | λxMι#λx'M'ι 
    ... | .(A' ∙ ι) | .(X (ι , fv M' - x')) | .(M' ∙ ι ≺+ (x' , v (X (ι , fv M' - x')))) | refl = refl , refl , refl
  ... | y≡y' , Mι≺+xy≡M'ι≺+xy' , Aι=A'ι with X (ι , fv M - x) | X (ι , fv M' - x') | lemma-χιₗ (fv M - x) | lemma-χιₗ (fv M' - x') | y≡y' 
  ... | y | .y | y#λxM | y#λx'M' | refl = ∼λ {M} {M'} {x} {x'} {y} {A} {A'} A∼A' y#λxM y#λx'M' M∼M'
    where    
    A∼A' : A ∼αₛ A'
    A∼A' = rec (length A) (s≤′s (m≤′m+n (length A) (length M))) A A' refl Aι=A'ι
    sMxy=sA+M : suc (length (M ∙ ι ≺+ (x , v y))) ≤′ suc (length A + length M)
    sMxy=sA+M rewrite coroRen {M} {x} {y} = s≤′s (n≤′m+n (length A) (length M))
    M∼M' : M [ x := v y ] ∼αₛ M' [ x' := v y ]
    M∼M' = rec (length (M ∙ (ι ≺+ (x , v y)))) sMxy=sA+M (M ∙ (ι ≺+ (x , v y))) (M' ∙ (ι ≺+ (x' , v y))) refl (cong (λ M → M ∙ ι)  Mι≺+xy≡M'ι≺+xy')
  iotaAlphaSt-aux .(suc (length A + length M)) rec (Π[ x ∶ A ] M) (Π[ x' ∶ A' ] M') refl ΠxMι≡Πx'M' with ΠxMι≡Πx'M'ι ΠxMι≡Πx'M' 
    where
    ΠxMι≡Πx'M'ι : Π[ x ∶ A ] M ∙ ι ≡ Π[ x' ∶ A' ] M' ∙ ι → X (ι , fv M - x) ≡ X (ι , fv M' - x') × M ∙ ι ≺+ (x , v (X (ι , fv M - x))) ≡ M' ∙ ι ≺+ (x' , v (X (ι , fv M' - x'))) × A ∙ ι ≡ A' ∙ ι
    ΠxMι≡Πx'M'ι ΠxMι#Πx'M'ι with A ∙ ι | X (ι , fv M - x) | M ∙ ι ≺+ (x , v (X (ι , fv M - x))) | ΠxMι#Πx'M'ι 
    ... | .(A' ∙ ι) | .(X (ι , fv M' - x')) | .(M' ∙ ι ≺+ (x' , v (X (ι , fv M' - x')))) | refl = refl , refl , refl
  ... | y≡y' , Mι≺+xy≡M'ι≺+xy' , Aι=A'ι with X (ι , fv M - x) | X (ι , fv M' - x') | lemma-χιₗ (fv M - x) | lemma-χιₗ (fv M' - x') | y≡y' 
  ... | y | .y | y#ΠxM | y#Πx'M' | refl = ∼Π {M} {M'} {x} {x'} {y} {A} {A'} A∼A' y#ΠxM y#Πx'M' M∼M'
    where    
    A∼A' : A ∼αₛ A'
    A∼A' = rec (length A) (s≤′s (m≤′m+n (length A) (length M))) A A' refl Aι=A'ι
    sMxy=sA+M : suc (length (M ∙ ι ≺+ (x , v y))) ≤′ suc (length A + length M)
    sMxy=sA+M rewrite coroRen {M} {x} {y} = s≤′s (n≤′m+n (length A) (length M))
    M∼M' : M [ x := v y ] ∼αₛ M' [ x' := v y ]
    M∼M' = rec (length (M ∙ (ι ≺+ (x , v y)))) sMxy=sA+M (M ∙ (ι ≺+ (x , v y))) (M' ∙ (ι ≺+ (x' , v y))) refl (cong (λ M → M ∙ ι)  Mι≺+xy≡M'ι≺+xy')

  iotaAlphaSt : {M M' : Λ} → M ∙ ι ≡ M' ∙ ι → M ∼αₛ M' 
  iotaAlphaSt {M} {M'} = (<′-rec _ iotaAlphaSt-aux) (length M) M M' refl

  infix 1 _∼α_⇂_
  _∼α_⇂_ : Sub → Sub → List 𝒱 → Set
  σ ∼α σ' ⇂ xs = ∀ x → x ∈ xs → σ x ∼α σ' x

  lemmaι∼α⇂ : {M : List 𝒱} → ι ∼α ι ⇂ M
  lemmaι∼α⇂ {M} x _ = ∼v 

  lemma≺+∼α⇂ : {x : 𝒱}{M : List 𝒱}{N P : Λ}{σ σ' : Sub} → σ ∼α σ' ⇂ M → N ∼α P → σ ‚ x := N ∼α σ' ‚ x := P ⇂ M
  lemma≺+∼α⇂ {x} σ∼ασ'⇂M N~P y y*M with x ≟ y
  ... | yes  _ = N~P 
  ... | no   _ = σ∼ασ'⇂M y y*M 

  comm-++ : ∀ xs ys z → (xs ++ ys) - z ≡ xs - z ++ ys - z
  comm-++ [] ys z = refl
  comm-++ (x ∷ xs) ys z with z ≟ x
  ... | yes _ = comm-++ xs ys z
  ... | no _ = cong (_∷_ x) (comm-++ xs ys z)

  ∉-≡ : ∀ y xs → y ∉ xs → xs - y ≡ xs
  ∉-≡ y [] _ = refl
  ∉-≡ y (x ∷ xs) y∉x::xs with y ≟ x
  ... | yes y=x = ⊥-elim (y∉x::xs (here y=x))
  ... | no y≠x = cong (_∷_ x) (∉-≡ y xs (λ y∈xs → ⊥-elim (y∉x::xs (there y∈xs))))

  lemma-concat-map : ∀ {σ x y} xs → y #⇂ (σ , xs - x) →  concat (map (fv ∘ (σ ‚ x := v y)) xs) - y ≡ concat (map (fv ∘ σ) (xs - x))
  lemma-concat-map [] _ = refl
  lemma-concat-map {σ} {x} {y} (z ∷ xs') y#σ⇂z::xs'-x with x ≟ z 
  ... | yes x=z with y ≟ y
  ... | yes _ = lemma-concat-map {σ} {x} {y} xs' y#σ⇂z::xs'-x
  ... | no y≢y = ⊥-elim (y≢y refl)  
  lemma-concat-map {σ} {x} {y} (z ∷ xs') y#σ⇂z::xs'-x | no x≠z = 
    begin
    (fv (σ z) ++ concat (map (fv ∘ (σ ‚ x := v y)) xs')) - y
    ≡⟨ comm-++ (fv (σ z)) (concat (map (fv ∘ (σ ‚ x := v y)) xs')) y ⟩
    (fv (σ z) - y) ++ (concat (map (fv ∘ (σ ‚ x := v y)) xs') - y)
    ≡⟨ cong₂ _++_ refl (lemma-concat-map xs' y#σ⇂xs'-x) ⟩
    (fv (σ z) - y) ++ concat (map (fv ∘ σ) (xs' - x))
    ≡⟨ cong₂ _++_ (∉-≡ y (fv (σ z)) y∉fvσz) refl ⟩        
    fv (σ z) ++ concat (map (fv ∘ σ) (xs' - x))
    ≡⟨⟩    
    concat (fv (σ z) ∷ map (fv ∘ σ) (xs' - x))        
    ≡⟨⟩    
    concat (map (fv ∘ σ) (z ∷ (xs' - x)))
    ∎
    where
    y#σ⇂xs'-x : y #⇂ (σ , xs' - x)
    y#σ⇂xs'-x w w∈xs'-x = y#σ⇂z::xs'-x w (there w∈xs'-x)
    y∉fvσz : y # σ z
    y∉fvσz = y#σ⇂z::xs'-x z (here refl)
    
  lemmafv∙ : ∀ {M σ} → fv (M ∙ σ) ≡ concat (map (fv ∘ σ) (fv M))
  lemmafv∙ {c _} = refl
  lemmafv∙ {v x} {σ} = sym (++-identityʳ (fv (σ x)))
  lemmafv∙ {λ[ x ∶ A ] M} {σ} =
    begin
    fv ((λ[ x ∶ A ] M) ∙ σ)
    ≡⟨⟩
    fv (A ∙ σ) ++ (fv (M ∙ σ ‚ x := v y) - y)
    ≡⟨ cong₂ _++_ (lemmafv∙ {A} {σ}) (cong (flip _-_ y) (lemmafv∙ {M} {σ ‚ x := v y})) ⟩
    concat (map (fv ∘ σ) (fv A)) ++ (concat (map (fv ∘ (σ ‚ x := v y)) (fv M)) - y)
    ≡⟨ cong (_++_ (concat (map (fv ∘ σ) (fv A)))) (lemma-concat-map (fv M) y#σ⇂fvM-x) ⟩         
    concat (map (fv ∘ σ) (fv A)) ++ concat (map (fv ∘ σ) (fv M - x))    
    ≡⟨ concat-++ (map (fv ∘ σ) (fv A)) (map (fv ∘ σ) (fv M - x)) ⟩ 
    concat (map (fv ∘ σ) (fv A) ++ map (fv ∘ σ) (fv M - x))
    ≡⟨ cong concat (sym (map-++-commute (fv ∘ σ) (fv A) (fv M - x))) ⟩ 
    concat (map (fv ∘ σ) (fv A ++ (fv M - x)))
    ≡⟨⟩
    concat (map (fv ∘ σ) (fv (λ[ x ∶ A ] M)))
    ∎
    where
    y : 𝒱
    y = X (σ , fv M - x)
    y#σ⇂fvM-x : y #⇂ (σ , (fv M - x))
    y#σ⇂fvM-x = Xfresh σ (fv M - x)    
  lemmafv∙ {Π[ x ∶ A ] M} {σ} = 
    begin
    fv ((Π[ x ∶ A ] M) ∙ σ)
    ≡⟨⟩
    fv (A ∙ σ) ++ (fv (M ∙ σ ‚ x := v y) - y)
    ≡⟨ cong₂ _++_ (lemmafv∙ {A} {σ}) (cong (flip _-_ y) (lemmafv∙ {M} {σ ‚ x := v y})) ⟩
    concat (map (fv ∘ σ) (fv A)) ++ (concat (map (fv ∘ (σ ‚ x := v y)) (fv M)) - y)
    ≡⟨ cong (_++_ (concat (map (fv ∘ σ) (fv A)))) (lemma-concat-map (fv M) y#σ⇂fvM-x) ⟩         
    concat (map (fv ∘ σ) (fv A)) ++ concat (map (fv ∘ σ) (fv M - x))    
    ≡⟨ concat-++ (map (fv ∘ σ) (fv A)) (map (fv ∘ σ) (fv M - x)) ⟩ 
    concat (map (fv ∘ σ) (fv A) ++ map (fv ∘ σ) (fv M - x))
    ≡⟨ cong concat (sym (map-++-commute (fv ∘ σ) (fv A) (fv M - x))) ⟩ 
    concat (map (fv ∘ σ) (fv A ++ (fv M - x)))
    ≡⟨⟩
    concat (map (fv ∘ σ) (fv (Π[ x ∶ A ] M)))
    ∎
    where
    y : 𝒱
    y = X (σ , fv M - x)
    y#σ⇂fvM-x : y #⇂ (σ , (fv M - x))
    y#σ⇂fvM-x = Xfresh σ (fv M - x) 
  lemmafv∙ {M · N} {σ} =
    begin
    fv (M · N ∙ σ)
    ≡⟨⟩
    fv (M ∙ σ) ++ fv (N ∙ σ)
    ≡⟨ cong₂ _++_ (lemmafv∙ {M} {σ}) (lemmafv∙ {N} {σ}) ⟩
    concat (map (fv ∘ σ) (fv M)) ++ concat (map (fv ∘ σ) (fv N))
    ≡⟨ concat-++ (map (fv ∘ σ) (fv M)) (map (fv ∘ σ) (fv N)) ⟩
    concat (map (fv ∘ σ) (fv M) ++ map (fv ∘ σ) (fv N))
    ≡⟨ cong concat (sym (map-++-commute (fv ∘ σ) (fv M) (fv N))) ⟩  
    concat (map (fv ∘ σ) (fv M ++ fv N))    
    ≡⟨⟩    
    concat (map (fv ∘ σ) (fv (M · N)))
    ∎

  concat-map-fv∘ι : ∀ xs → concat (map (fv ∘ ι) xs) ≡ xs
  concat-map-fv∘ι [] = refl
  concat-map-fv∘ι (x ∷ xs') = cong (_∷_ x) (concat-map-fv∘ι xs')

  lemmafv∉ : ∀ {x y M} → y ∉ fv M - x → fv (M [ x := v y ]) - y ≡ fv M - x
  lemmafv∉ {x} {y} {M} y∉fvM-x =
    begin
    fv (M [ x := v y ]) - y
    ≡⟨ cong (flip _-_ y) (lemmafv∙ {M} {ι ‚ x := v y}) ⟩    
    concat (map (fv ∘ (ι ‚ x := v y)) (fv M)) - y
    ≡⟨ lemma-concat-map {ι} {x} {y} (fv M) (lemma#→ι#⇂ {y} {x} {fv M} y∉fvM-x) ⟩
    concat (map (fv ∘ ι) (fv M - x))
    ≡⟨ concat-map-fv∘ι (fv M - x) ⟩
    fv M - x
    ∎ 

  M∼M'→fvM≡fvM' : ∀ {M M'} → M ∼α M' → fv M ≡ fv M'
  M∼M'→fvM≡fvM' ∼c = refl
  M∼M'→fvM≡fvM' ∼v = refl
  M∼M'→fvM≡fvM' (∼· e1 e2) = cong₂ _++_ (M∼M'→fvM≡fvM' e1) (M∼M'→fvM≡fvM' e2)
  M∼M'→fvM≡fvM' (∼λ {x} {x'} {y} {A} {A'} {M} {M'} A∼A' y∉fvM-x y∉fvM'-x' M[x=y]∼M'[x'=y]) =
    begin
    fv (λ[ x ∶ A ] M)
    ≡⟨⟩
    fv A ++ (fv M - x)    
    ≡⟨ cong (_++_ (fv A)) (sym (lemmafv∉ {x} {y} {M} y∉fvM-x)) ⟩    
    fv A ++ (fv (M [ x := v y ]) - y)
    ≡⟨ cong₂ _++_ (M∼M'→fvM≡fvM' A∼A') (cong (flip _-_ y) (cong fv M[x=y]∼M'[x'=y])) ⟩
    fv A' ++ (fv (M' [ x' := v y ]) - y)    
    ≡⟨ cong (_++_ (fv A')) (lemmafv∉ {x'} {y} {M'} y∉fvM'-x') ⟩
    fv A' ++ (fv M' - x')
    ≡⟨⟩ 
    fv (λ[ x' ∶ A' ] M')
    ∎
  M∼M'→fvM≡fvM' (∼Π {x} {x'} {y} {A} {A'} {M} {M'} A∼A' y∉fvM-x y∉fvM'-x' M[x=y]∼M'[x'=y]) =
    begin
    fv (Π[ x ∶ A ] M)
    ≡⟨⟩
    fv A ++ (fv M - x)    
    ≡⟨ cong (_++_ (fv A)) (sym (lemmafv∉ {x} {y} {M} y∉fvM-x)) ⟩    
    fv A ++ (fv (M [ x := v y ]) - y)
    ≡⟨ cong₂ _++_ (M∼M'→fvM≡fvM' A∼A') (cong (flip _-_ y) (cong fv M[x=y]∼M'[x'=y])) ⟩
    fv A' ++ (fv (M' [ x' := v y ]) - y)    
    ≡⟨ cong (_++_ (fv A')) (lemmafv∉ {x'} {y} {M'} y∉fvM'-x') ⟩
    fv A' ++ (fv M' - x')
    ≡⟨⟩ 
    fv (Π[ x' ∶ A' ] M')
    ∎

  lemmaM∼M'→free← : ∀ {M M' z} → M ∼α M' → z * M' → z * M
  lemmaM∼M'→free← M∼M' x*M' rewrite M∼M'→fvM≡fvM' M∼M' = x*M'

  lemmaM∼M'→fresh→ : ∀ {M M' z} → M ∼α M' → z # M → z # M'
  lemmaM∼M'→fresh→ M∼M' z#M z*M' = ⊥-elim (z#M (lemmaM∼M'→free← M∼M' z*M'))

  ++-injectiveˡ : (xs ys ys' : List 𝒱) → xs ++ ys ≡ xs ++ ys' → ys ≡ ys'
  ++-injectiveˡ [] ys ys' e = e
  ++-injectiveˡ (x ∷ xs') ys ys' e = ++-injectiveˡ xs' ys ys' (∷-injectiveʳ e)

  ∼α⇒∉- : ∀ {x y A B M N} → λ[ x ∶ A ] M ∼α λ[ y ∶ B ] N → x ∉ fv N - y
  ∼α⇒∉- {x} {y} {A} {B} {M} {N} λxM∼λyN@(∼λ A∼B _ _ _) = subst (λ l → x ∉ l) e3 (∉- {x} (fv M))
    where
    e1 : fv A ++ (fv M - x) ≡ fv B ++ (fv N - y)
    e1 = M∼M'→fvM≡fvM' λxM∼λyN
    e2 : fv A ≡ fv B
    e2 = M∼M'→fvM≡fvM' A∼B
    e3 : fv M - x ≡ fv N - y
    e3 = ++-injectiveˡ (fv A) (fv M - x) (fv N - y) (subst (λ l → fv A ++ (fv M - x) ≡ l ++ (fv N - y)) (sym e2) e1)

  ∼α⇒∉-Π : ∀ {x y A B M N} → Π[ x ∶ A ] M ∼α Π[ y ∶ B ] N → x ∉ fv N - y
  ∼α⇒∉-Π {x} {y} {A} {B} {M} {N} ΠxM∼ΠyN@(∼Π A∼B _ _ _) = subst (λ l → x ∉ l) e3 (∉- {x} (fv M))
    where
    e1 : fv A ++ (fv M - x) ≡ fv B ++ (fv N - y)
    e1 = M∼M'→fvM≡fvM' ΠxM∼ΠyN
    e2 : fv A ≡ fv B
    e2 = M∼M'→fvM≡fvM' A∼B
    e3 : fv M - x ≡ fv N - y
    e3 = ++-injectiveˡ (fv A) (fv M - x) (fv N - y) (subst (λ l → fv A ++ (fv M - x) ≡ l ++ (fv N - y)) (sym e2) e1)

  CommAlpha : (Λ → Λ → Set) → Set
  CommAlpha _𝒮_ = ∀ {M N P} → M ∼α N → N 𝒮 P → ∃ λ Q → M 𝒮 Q × Q ∼α P