---

Step * of Lemma setmemfunclemma_ext

∀x1,s1,x2,s2:coSet{i:l}.  (seteq(x1;x2) ⇒ seteq(s1;s2) ⇒ {(x1 ∈ s1) ⇐⇒ (x2 ∈ s2)})
BY
{ Extract of Obid: setmemfunclemma
  not unfolding  seteqweaken seteqinv seteqtrans seq-add seq-nil copath-hd copath-tl copath-cons coW-trans copath-nil
  finishing with Auto
  normalizes to:
  
  λx1,s1,x2,s2,%,%1. <λ%5.let x,y = s2 
                          in let b,y1 = %5 
                             in let q1,y2 = %1 
                                            <2
                                            , λi.if i=0
                                                 then <(), ()>
                                                 else if i - 1=0 then <copath-cons(b;()), ()> else (⋅ (i - 1 - 1))
                                            > 
                                in <copath-hd(y2)
                                   , seteqtrans() x2 x1 (y copath-hd(y2)) (seteqinv() x1 x2 %) 
                                     coW-trans(y1;
                                               λmoves.let u,v = %1 
                                                                let k,g = moves 
                                                                in <(k + 1) + 1
                                                                   , λi.if i=0
                                                                        then <(), ()>
                                                                        else if i - 1=0
                                                                             then <copath-cons(b;()), ()>
                                                                             else let u,v = g (i - 1 - 1) 
                                                                                  in <copath-cons(b;u)
                                                                                     , copath-cons(copath-hd(y2);v)
                                                                                     >
                                                                   > 
                                                      in <copath-tl(u), copath-tl(v)>)
                                   >
                     , λ%5.let x,y = s1 
                           in let b,y1 = %5 
                              in let u,y2 = %1 
                                            <2
                                            , λi.if i=0
                                                 then <(), ()>
                                                 else if i - 1=0
                                                      then <(), copath-cons(b;())>
                                                      else let u,v = ⋅ (i - 1 - 1) 
                                                           in <v, u>
                                            > 
                                 in <copath-hd(u)
                                    , seteqtrans() x1 x2 (y copath-hd(u)) % 
                                      coW-trans(y1;
                                                λmoves.let u,v = %1 
                                                                 let k,g = moves 
                                                                 in <(k + 1) + 1
                                                                    , λi.if i=0
                                                                         then <(), ()>
                                                                         else if i - 1=0
                                                                              then <(), copath-cons(b;())>
                                                                              else let u@0,v = g (i - 1 - 1) 
                                                                                   in <copath-cons(copath-hd(u);v)
                                                                                      , copath-cons(b;u@0)
                                                                                      >
                                                                    > 
                                                       in <copath-tl(v), copath-tl(u)>)
                                    >
                     > }

---

Latex:

---

Latex:
\mforall{}x1,s1,x2,s2:coSet\{i:l\}.    (seteq(x1;x2)  {}\mRightarrow{}  seteq(s1;s2)  {}\mRightarrow{}  \{(x1  \mmember{}  s1)  \mLeftarrow{}{}\mRightarrow{}  (x2  \mmember{}  s2)\})


By

---

Latex:
...

---

Home Index