Step
*
1
2
of Lemma
decidable__equal_fset
1. [T] : Type
2. ∀x,y:T. Dec(x = y ∈ T)@i
3. xs : fset(T)@i
4. ys : fset(T)@i
5. EqDecider(T)
⊢ Dec(xs = ys ∈ fset(T))
BY
{ (RenameVar `eq' (-1) THEN Assert ⌜xs = ys ∈ fset(T)
⇐⇒ xs ⊆ ys ∧ ys ⊆ xs⌝⋅) }
1
.....assertion.....
1. [T] : Type
2. ∀x,y:T. Dec(x = y ∈ T)@i
3. xs : fset(T)@i
4. ys : fset(T)@i
5. eq : EqDecider(T)
⊢ xs = ys ∈ fset(T)
⇐⇒ xs ⊆ ys ∧ ys ⊆ xs
2
1. [T] : Type
2. ∀x,y:T. Dec(x = y ∈ T)@i
3. xs : fset(T)@i
4. ys : fset(T)@i
5. eq : EqDecider(T)
6. xs = ys ∈ fset(T)
⇐⇒ xs ⊆ ys ∧ ys ⊆ xs
⊢ Dec(xs = ys ∈ fset(T))
Latex:
Latex:
1. [T] : Type
2. \mforall{}x,y:T. Dec(x = y)@i
3. xs : fset(T)@i
4. ys : fset(T)@i
5. EqDecider(T)
\mvdash{} Dec(xs = ys)
By
Latex:
(RenameVar `eq' (-1) THEN Assert \mkleeneopen{}xs = ys \mLeftarrow{}{}\mRightarrow{} xs \msubseteq{} ys \mwedge{} ys \msubseteq{} xs\mkleeneclose{}\mcdot{})
Home
Index