Step
*
1
3
of Lemma
list-powerset_wf
1. T : Type
2. eq : EqDecider(T)
3. p : fset(fset(T))
⊢ istype(∀x:fset(T). (x ∈ p
⇐⇒ x ⊆ {}))
BY
{ Auto }
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. p : fset(fset(T))
\mvdash{} istype(\mforall{}x:fset(T). (x \mmember{} p \mLeftarrow{}{}\mRightarrow{} x \msubseteq{} \{\}))
By
Latex:
Auto
Home
Index