---

Step * of Lemma tagged-true-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T × 𝔹)]. ∀[e:E].
  Tagged_tt(X)(e) ~ fst(X(e)) supposing ↑e ∈b Tagged_tt(X)
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
6. ↑e ∈b Tagged_tt(X)
⊢ λp.if snd(p) then {fst(p)} else {} fi [X](e) ~ fst(X(e))

---

Latex:

---

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


By

---

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

---

Home Index