---

Step * of Lemma assoced_weakening

∀a,b:ℤ.  a ~ b supposing a = b ∈ ℤ
BY
{ ((Unfold `assoced` 0 THEN GenRepD) THENA Auto) }

1
1. a : ℤ
2. b : ℤ
3. a = b ∈ ℤ
⊢ a | b

2
1. a : ℤ
2. b : ℤ
3. a = b ∈ ℤ
⊢ b | a

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    a  \msim{}  b  supposing  a  =  b


By

---

Latex:
((Unfold  `assoced`  0  THEN  GenRepD)  THENA  Auto)

---

Home Index