diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-24 18:20:43 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-24 18:20:43 +0200 |
| commit | 6df3f662f0f23e837b70ef1f4a8b8dde4a7aa521 (patch) | |
| tree | c56ca4d707e88d49c0f52e99d5e1c07edb58e3fe /Nominal/Instances/Abstraction.lean | |
| parent | ac2363701c3d2a03116af449ca7bc4f918fbfda7 (diff) | |
use simp only everywhere except for last goal
Diffstat (limited to 'Nominal/Instances/Abstraction.lean')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 891f00f..d7fade9 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -88,7 +88,7 @@ private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred rw [AlphaEqPred, AlphaEqPred] intro h have h' : π • ⸨a, x.fst.atom⸩ • x.fst.body = π • ⸨a, x.snd.atom⸩ • x.snd.body := by congr - simp [smul_smul, FPerm.mul_swap_eq_swap_mul] at h' + simp only [smul_smul, FPerm.mul_swap_eq_swap_mul] at h' simpa [smul_smul] lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by @@ -96,14 +96,14 @@ lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ rw [alpha_eq_iff_pred, this] apply Equivariance.for_fresh_iff_exists exact alpha_eq_pred_equivariant - simp only [Prod.fresh, AlphaEqPred, @and_assoc] + simp [Prod.fresh, AlphaEqPred, @and_assoc] lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by suffices (∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∀ c, c # (x, y) → AlphaEqPred c (x, y)) by rw [alpha_eq_iff_pred, this] apply Equivariance.for_fresh_iff_all exact alpha_eq_pred_equivariant - simp only [Prod.fresh, AlphaEqPred] + simp [Prod.fresh, AlphaEqPred] lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.atom = y.atom ∧ x.body = y.body) ∨ (x.atom ≠ y.atom ∧ x.atom # y ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by sorry |