---

Step * of Lemma f-union-subset

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[x,y,z:fset(A)].  uiff(x ⋃ y ⊆ z;x ⊆ z ∧ y ⊆ z)
BY
{ (Auto
   THEN Unfold `f-subset` 0
   THEN Unfold `f-subset` -1
   THEN Auto
   THEN Try ((BackThruSomeHyp THEN BLemma `member-fset-union` THEN Auto))) }

1
1. A : Type
2. eq : EqDecider(A)
3. x : fset(A)
4. y : fset(A)
5. z : fset(A)
6. x ⊆ z
7. ∀a:A. a ∈ z supposing a ∈ y
8. a : A@i
9. a ∈ x ⋃ y
⊢ a ∈ z

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[x,y,z:fset(A)].    uiff(x  \mcup{}  y  \msubseteq{}  z;x  \msubseteq{}  z  \mwedge{}  y  \msubseteq{}  z)


By

---

Latex:
(Auto
  THEN  Unfold  `f-subset`  0
  THEN  Unfold  `f-subset`  -1
  THEN  Auto
  THEN  Try  ((BackThruSomeHyp  THEN  BLemma  `member-fset-union`  THEN  Auto)))

---

Home Index