Step
*
1
of Lemma
free-dl-1
1. T : Type
2. eq : EqDecider(T)
3. x : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
4. {} ∈ x
⊢ x = {{}} ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
BY
{ DVar `x' }
1
1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T))
4. ↑fset-antichain(eq;x)
5. {} ∈ x
⊢ x = {{}} ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. x : \{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\}
4. \{\} \mmember{} x
\mvdash{} x = \{\{\}\}
By
Latex:
DVar `x'
Home
Index