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