---

Step * of Lemma fset-item-member

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)].  item(s) ∈ s supposing ||s|| = 1 ∈ ℤ
BY
{ (Auto
   THEN InstLemma `fset-item_wf` [⌜T⌝;⌜eq⌝;⌜s⌝]⋅
   THEN Auto
   THEN All (Unfold `fset-item`)
   THEN Unfold `fset-member` 0
   THEN (Assert ⌜hd(s) ∈b s = tt⌝⋅ THEN Try ((HypSubst' (-1) 0 THEN Auto)))⋅) }

1
.....assertion..... 
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. ||s|| = 1 ∈ ℤ
5. hd(s) ∈ T
⊢ hd(s) ∈b s = tt

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[s:fset(T)].    item(s)  \mmember{}  s  supposing  ||s||  =  1


By

---

Latex:
(Auto
  THEN  InstLemma  `fset-item\_wf`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  All  (Unfold  `fset-item`)
  THEN  Unfold  `fset-member`  0
  THEN  (Assert  \mkleeneopen{}hd(s)  \mmember{}\msubb{}  s  =  tt\mkleeneclose{}\mcdot{}  THEN  Try  ((HypSubst'  (-1)  0  THEN  Auto)))\mcdot{})

---

Home Index