---

Step * of Lemma tagged-val_wf2

∀[B:Type]. ∀[z:Atom]. ∀[x:z:B].  x.val ∈ B supposing x.tag = z ∈ Atom
BY
{ xxxRepeatFor 3 ((D 0 THENA (Auto THEN DVar `x' THEN RepUR ``tagged-tag`` 0 THEN Auto)))xxx }

1
1. B : Type
2. z : Atom
3. x : z:B
⊢ x.val ∈ B supposing x.tag = z ∈ Atom

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}[z:Atom].  \mforall{}[x:z:B].    x.val  \mmember{}  B  supposing  x.tag  =  z


By

---

Latex:
xxxRepeatFor  3  ((D  0  THENA  (Auto  THEN  DVar  `x'  THEN  RepUR  ``tagged-tag``  0  THEN  Auto)))xxx

---

Home Index