---

Step * 2 of Lemma ite_wf


1. y1 : Unit
2. T : Type
3. x : T supposing False
4. y : T supposing ¬False
⊢ y ∈ T
BY
{ (D 4 THEN With ⌜λx.Ax⌝ (DVar `y')⋅ THEN Auto THEN RepUR ``not implies`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  y1  :  Unit
2.  T  :  Type
3.  x  :  T  supposing  False
4.  y  :  T  supposing  \mneg{}False
\mvdash{}  y  \mmember{}  T


By

---

Latex:
(D  4  THEN  With  \mkleeneopen{}\mlambda{}x.Ax\mkleeneclose{}  (DVar  `y')\mcdot{}  THEN  Auto  THEN  RepUR  ``not  implies``  0  THEN  Auto)

---

Home Index