---

Step * 1 1 of Lemma fl1-not-1


1. I : fset(ℕ)
2. x : names(I)
3. {inr x } = {} ∈ fset(names(I) + names(I))
⊢ False
BY
{ (Assert inr x  ∈ {inr x } BY
         Auto) }

1
1. I : fset(ℕ)
2. x : names(I)
3. {inr x } = {} ∈ fset(names(I) + names(I))
4. inr x  ∈ {inr x }
⊢ False

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  names(I)
3.  \{inr  x  \}  =  \{\}
\mvdash{}  False


By

---

Latex:
(Assert  inr  x    \mmember{}  \{inr  x  \}  BY
              Auto)

---

Home Index