update lean

1 files changed, 9 insertions, 13 deletions

diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean
index 91f4fb8..7af82cd 100644
--- a/Nominal/LambdaCalculus/Terms.lean
+++ b/Nominal/LambdaCalculus/Terms.lean
@@ -53,40 +53,37 @@ instance Preterm.instSetoidEquivariant : Rel.Equivariant Var setoid.r := by
     exact h
 
 /-- Define λ-terms as the quotient Preterm/≈. -/
-def Term := Quotient Preterm.setoid
+abbrev Term := Quotient Preterm.setoid
 
 namespace Term
 
-/-- The equivalence class of a λ-preterm. -/
-abbrev mk : Preterm → Term := Quotient.mk Preterm.setoid
-
 instance : NominalSet Var Term := Quotient.instNominalSet Var
 
 @[simp]
-lemma smul {π : FPerm Var} {t : Preterm} : π • Term.mk t = Term.mk (π • t) := by congr
+lemma smul {π : FPerm Var} {t : Preterm} : π • (⟦t⟧ : Term) = ⟦π • t⟧ := by congr
 
 private lemma alpha_eq {t u : Preterm} : t ≈ u ↔ AlphaEq t u := by rfl
 
-lemma eq_iff_alpha_eq {t u : Preterm} : mk t = mk u ↔ t ≈ u := by
+lemma eq_iff_alpha_eq {t u : Preterm} : (⟦t⟧ : Term) = (⟦u⟧ : Term) ↔ t ≈ u := by
   rw [Quotient.eq_iff_equiv]
 
-def var : Var → Term := fun x => mk (.var x)
+def var : Var → Term := fun x => ⟦.var x⟧
 
 def abs : Var → Term → Term := fun x =>
   Quotient.lift
-    (fun t => mk (.abs x t))
+    (fun t => ⟦.abs x t⟧)
     (by intro t t'; rw [eq_iff_alpha_eq]; exact AlphaEq.cong_abs)
 
 def app : Term → Term → Term :=
   Quotient.lift₂
-    (fun t u => mk (.app t u))
+    (fun t u => ⟦.app t u⟧)
     (by intro t₁ t₂ u₁ u₂; rw [eq_iff_alpha_eq]; exact AlphaEq.cong_app)
 
 @[simp]
-lemma abs_preterm {x : Var} {t : Preterm} : abs x (mk t) = mk (.abs x t) := rfl
+lemma abs_preterm {x : Var} {t : Preterm} : abs x ⟦t⟧ = ⟦.abs x t⟧ := rfl
 
 @[simp]
-lemma app_preterm {t u : Preterm} : app (mk t) (mk u) = mk (.app t u) := rfl
+lemma app_preterm {t u : Preterm} : app ⟦t⟧ ⟦u⟧ = ⟦.app t u⟧ := rfl
 
 /-- Alternative characterization of α-equivalence for each preterm constructor. -/
 inductive AlphaEq' : Preterm → Preterm → Prop where
@@ -242,7 +239,6 @@ lemma eq_abs {x y : Var} {t u : Term} : Term.abs x t = Term.abs y u ↔ ⟪x⟫
   obtain ⟨u', hu'⟩ := u.exists_rep
   simp only [abs, ← ht', Quotient.lift_mk, ← hu']
   rw [Quotient.eq_iff_equiv, alpha_eq_abs]
-  rfl
 
 /-- Alternative characterization of α-equivalence for application preterms. -/
 lemma alpha_eq_app {t₁ t₂ u₁ u₂ : Preterm} : Preterm.app t₁ t₂ ≈ Preterm.app u₁ u₂ ↔ t₁ ≈ u₁ ∧ t₂ ≈ u₂ := by
@@ -295,7 +291,7 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term
       (by
         intro t u htu
         rw [alpha_eq, alpha_eq_iff] at htu
-        cases htu <;> simp only [Sum.inr.injEq, Sum.inl.injEq, *]; assumption)
+        cases htu <;> simp [*])
     invFun
       | .inl x => .var x
       | .inr (.inl x) => Quotient.liftOn x