---

Step * 1 of Lemma tagged-val_wf2


1. B : Type
2. z : Atom
3. x : z:B
⊢ x.val ∈ B supposing x.tag = z ∈ Atom
BY
{ (Unfolds ``tagged-tag tagged-val`` 0 THEN D (-1) THEN Reduce 0 THEN SplitOnHypITE -1  THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  B  :  Type
2.  z  :  Atom
3.  x  :  z:B
\mvdash{}  x.val  \mmember{}  B  supposing  x.tag  =  z


By

---

Latex:
(Unfolds  ``tagged-tag  tagged-val``  0  THEN  D  (-1)  THEN  Reduce  0  THEN  SplitOnHypITE  -1    THEN  Auto)\mcdot{}

---

Home Index