---

Step * 1 of Lemma fl0-not-1


1. I : fset(ℕ)
2. x : names(I)
3. {{inl x}} = {{}} ∈ fset(fset(names(I) + names(I)))
⊢ False
BY
{ ((InstLemma `fset-singletons-equal` [⌜fset(names(I) + names(I))⌝;
    ⌜deq-fset(union-deq(names(I);names(I);NamesDeq;NamesDeq))⌝]⋅
    THENA Auto
    )
   THEN (RWO "-1" (-2) THENA Auto)
   THEN Thin (-1)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `fset-singletons-equal`  [\mkleeneopen{}fset(names(I)  +  names(I))\mkleeneclose{};
    \mkleeneopen{}deq-fset(union-deq(names(I);names(I);NamesDeq;NamesDeq))\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index