---

Step * of Lemma seteqinv1_ext

No Annotations
∀s1,s2:coSet{i:l}.  (seteq(s1;s2) ⇒ seteq(s2;s1))
BY
{ Extract of Obid: seteqinv1
  not unfolding  seq-comp
  finishing with Auto
  normalizes to:
  
  λ_,_,eq,moves. let u,v = eq λp.let u,v = p in <v, u> o moves in <v, u> }

---

Latex:

---

Latex:
No  Annotations
\mforall{}s1,s2:coSet\{i:l\}.    (seteq(s1;s2)  {}\mRightarrow{}  seteq(s2;s1))


By

---

Latex:
Extract  of  Obid:  seteqinv1
not  unfolding    seq-comp
finishing  with  Auto
normalizes  to:

\mlambda{}$_{}$,$_{}$,eq,moves.  let  u,v  =  eq  \mlambda{}p.let  u,v  =  p  in  <v,  u>\000C  o  moves  in  <v,  u>

---

Home Index