---

Step * of Lemma fset-add-as-cons

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[x:T].  (fset-add(eq;x;s) = [x / s] ∈ fset(T))
BY
{ (Auto THEN Assert ⌜[x / s] ∈ fset(T)⌝⋅) }

1
.....assertion..... 
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. x : T
⊢ [x / s] ∈ fset(T)

2
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. x : T
5. [x / s] ∈ fset(T)
⊢ fset-add(eq;x;s) = [x / s] ∈ fset(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[s:fset(T)].  \mforall{}[x:T].    (fset-add(eq;x;s)  =  [x  /  s])


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}[x  /  s]  \mmember{}  fset(T)\mkleeneclose{}\mcdot{})

---

Home Index