---

Step * of Lemma is-tagged-true

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T × 𝔹)]. ∀[e:E].
  uiff(↑e ∈b Tagged_tt(X);(↑e ∈b X) ∧ (↑(snd(X(e)))))
BY
{ ((UnivCD THENA Auto) THEN Unfold `es-tagged-true-class` 0) }

1
1. Info : Type
2. es : EO+(Info)
3. T : Type
4. X : EClass(T × 𝔹)
5. e : E
⊢ uiff(↑e ∈b λp.if snd(p) then {fst(p)} else {} fi [X];(↑e ∈b X) ∧ (↑(snd(X(e)))))

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:EClass(T  \mtimes{}  \mBbbB{})].  \mforall{}[e:E].
    uiff(\muparrow{}e  \mmember{}\msubb{}  Tagged\_tt(X);(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\muparrow{}(snd(X(e)))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `es-tagged-true-class`  0)

---

Home Index