Prove alpha equivalence is symmetric.

1 files changed, 7 insertions, 1 deletions

diff --git a/src/Data/Type/Properties.agda b/src/Data/Type/Properties.agda
index ecfbc92..28667fa 100644
--- a/src/Data/Type/Properties.agda
+++ b/src/Data/Type/Properties.agda
@@ -18,7 +18,7 @@ open import Data.List.Relation.Unary.Any using (Any)
 open import Data.Nat using (ℕ; _<_; _≟_; _+_)
 open import Data.Nat.Induction using (<-wellFounded)
 open import Data.Nat.Properties
-open import Data.Product using () renaming (_,_ to _,′_)
+open import Data.Product using (∃₂) renaming (_,_ to _,′_)
 open import Data.Sum as ⊎ using (_⊎_; fromInj₁; fromInj₂; [_,_])
 open import Data.Type mkFresh
 open import Induction.WellFounded as Wf using (WfRec)
@@ -246,3 +246,9 @@ free-≈ (all {α} {A} {β} {B} A≈B) = begin
   go (bin ⊗ A B) hyp = bin (hyp A (m≤m+n _ _)) (hyp B (m<n+m _ 0<1+n))
   go (all α A)   hyp =
     all (λ _ _ → hyp _ (P.subst (_< _) (sym (size-rename _ A)) (n<1+n _)))
+
+≈-sym : Symmetric _≈_
+≈-sym (var α)       = var α
+≈-sym unit          = unit
+≈-sym (bin A≈C B≈D) = bin (≈-sym A≈C) (≈-sym B≈D)
+≈-sym (all A≈B)     = all (λ γ∉∀β∙B γ∉∀α∙A → ≈-sym (A≈B γ∉∀α∙A γ∉∀β∙B))