---

Step * 1 2 of Lemma list-powerset_wf


1. T : Type
2. eq : EqDecider(T)
⊢ ∀x:fset(T). (x ∈ {{}} ⇐⇒ x ⊆ {})
BY
{ ((D 0 THENA Auto)
   THEN (RWO "member-fset-singleton" 0
         THENA (InstLemma `fset-member_wf` [⌜fset(T)⌝;⌜deq-fset(eq)⌝;⌜x⌝;⌜{{}}⌝]⋅ THEN Auto)
         )
   ) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : fset(T)
⊢ x = {} ∈ fset(T) ⇐⇒ x ⊆ {}

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
\mvdash{}  \mforall{}x:fset(T).  (x  \mmember{}  \{\{\}\}  \mLeftarrow{}{}\mRightarrow{}  x  \msubseteq{}  \{\})


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (RWO  "member-fset-singleton"  0
              THENA  (InstLemma  `fset-member\_wf`  [\mkleeneopen{}fset(T)\mkleeneclose{};\mkleeneopen{}deq-fset(eq)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}\{\{\}\}\mkleeneclose{}]\mcdot{}  THEN  Auto)
              )
  )

---

Home Index