---

Step * of Lemma member-fset-intersection

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:fset(T)]. ∀[x:T].  uiff(x ∈ a ⋂ b;x ∈ a ∧ x ∈ b)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `fset-intersection` 0
   THEN (RWO "member-fset-filter" 0 THENA Auto)
   THEN Unfold `guard` 0
   THEN (RWO "assert-deq-fset-member" 0 THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. a : fset(T)
4. b : fset(T)
5. x : T
⊢ uiff(x ∈ a ∧ x ∈ b;x ∈ a ∧ x ∈ b)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[a,b:fset(T)].  \mforall{}[x:T].    uiff(x  \mmember{}  a  \mcap{}  b;x  \mmember{}  a  \mwedge{}  x  \mmember{}  b)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `fset-intersection`  0
  THEN  (RWO  "member-fset-filter"  0  THENA  Auto)
  THEN  Unfold  `guard`  0
  THEN  (RWO  "assert-deq-fset-member"  0  THENA  Auto))

---

Home Index