---

Step * of Lemma member-ite

∀b:𝔹. ∀[T:Type]. ∀A,B:T List. ∀x:T.  ((x ∈ if b then A else B fi ) ⇐⇒ ((↑b) ∧ (x ∈ A)) ∨ ((¬↑b) ∧ (x ∈ B)))
BY
{ ((D 0 THENA Auto)
   THEN AutoBoolCase ⌈b⌉⋅
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN Try (((D (-2)) THEN Complete (Auto)))
   THEN Try ((OrLeft THEN Complete (Auto)))
   THEN Try ((OrRight THEN Auto THEN D 0 THEN Complete (Auto)))) }

---

Latex:


\mforall{}b:\mBbbB{}
    \mforall{}[T:Type]
        \mforall{}A,B:T  List.  \mforall{}x:T.    ((x  \mmember{}  if  b  then  A  else  B  fi  )  \mLeftarrow{}{}\mRightarrow{}  ((\muparrow{}b)  \mwedge{}  (x  \mmember{}  A))  \mvee{}  ((\mneg{}\muparrow{}b)  \mwedge{}  (x  \mmember{}  B)))


By

((D  0  THENA  Auto)
  THEN  AutoBoolCase  \mkleeneopen{}b\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  Try  (((D  (-2))  THEN  Complete  (Auto)))
  THEN  Try  ((OrLeft  THEN  Complete  (Auto)))
  THEN  Try  ((OrRight  THEN  Auto  THEN  D  0  THEN  Complete  (Auto))))

---

Home Index