---

Step * of Lemma fset-intersection-associative

∀[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x,y,z:fset(A)].  (x ⋂ y ⋂ z = x ⋂ y ⋂ z ∈ fset(A))
BY
{ ((Auto THEN (Using [`eq',⌜eqa⌝] (BLemma `fset-extensionality` )⋅ THENA Auto))
   THEN Intro
   THEN RepeatFor 2 ((RWO "member-fset-intersection" 0⋅ THENA Auto))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[x,y,z:fset(A)].    (x  \mcap{}  y  \mcap{}  z  =  x  \mcap{}  y  \mcap{}  z)


By

---

Latex:
((Auto  THEN  (Using  [`eq',\mkleeneopen{}eqa\mkleeneclose{}]  (BLemma  `fset-extensionality`  )\mcdot{}  THENA  Auto))
  THEN  Intro
  THEN  RepeatFor  2  ((RWO  "member-fset-intersection"  0\mcdot{}  THENA  Auto))
  THEN  Auto)

---

Home Index