Step * of Lemma member-ite

b:𝔹. ∀[T:Type]. ∀A,B:T List. ∀x:T.  ((x ∈ if then else fi ⇐⇒ ((↑b) ∧ (x ∈ A)) ∨ ((¬↑b) ∧ (x ∈ B)))
BY
((D 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 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