---

Step * of Lemma assoced_equiv_rel

EquivRel(ℤ;x,y.x ~ y)
BY
{ % With better HO matching, could fold directly the
symmetrize relation here %
Assert ⌜EquivRel(ℤ;x,y.Symmetrize(u,v.u | v;x;y))⌝ }

1
.....assertion..... 
EquivRel(ℤ;x,y.Symmetrize(u,v.u | v;x;y))

2
1. EquivRel(ℤ;x,y.Symmetrize(u,v.u | v;x;y))
⊢ EquivRel(ℤ;x,y.x ~ y)

---

Latex:

---

Latex:
EquivRel(\mBbbZ{};x,y.x  \msim{}  y)


By

---

Latex:
\%  With  better  HO  matching,  could  fold  directly  the
symmetrize  relation  here  \%
Assert  \mkleeneopen{}EquivRel(\mBbbZ{};x,y.Symmetrize(u,v.u  |  v;x;y))\mkleeneclose{}

---

Home Index