---

Step * of Lemma cons-wf-fset

∀[T:Type]. ∀[s:fset(T)]. ∀[x:T].  ([x / s] ∈ fset(T))
BY
{ (Intros THEN Unhide THEN D 2 THEN EqTypeCD THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. s : Base
3. s1 : Base
4. s = s1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
5. s ∈ T List
6. s1 ∈ T List
7. set-equal(T;s;s1)
8. x : T
⊢ set-equal(T;[x / s];[x / s1])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[s:fset(T)].  \mforall{}[x:T].    ([x  /  s]  \mmember{}  fset(T))


By

---

Latex:
(Intros  THEN  Unhide  THEN  D  2  THEN  EqTypeCD  THEN  Auto)

---

Home Index