---

Step * of Lemma bag-member-ifthenelse

∀[T:Type]. ∀[as,bs:bag(T)]. ∀[x:T].  ∀b:𝔹. uiff(x ↓∈ if b then as else bs fi ;if b then x ↓∈ as else x ↓∈ bs fi )
BY
{ ((UnivCD THENA Auto) THEN AutoSplit THEN Auto THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:bag(T)].  \mforall{}[x:T].
    \mforall{}b:\mBbbB{}.  uiff(x  \mdownarrow{}\mmember{}  if  b  then  as  else  bs  fi  ;if  b  then  x  \mdownarrow{}\mmember{}  as  else  x  \mdownarrow{}\mmember{}  bs  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  AutoSplit  THEN  Auto  THEN  Unhide  THEN  Auto)

---

Home Index