diff options
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 |