---

Step * of Lemma bag-maximal?-single

∀[T:Type]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[v,x:T].  uiff(↑bag-maximal?({v};x;R);↑(R x v))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``bag-maximal? single-bag bag-accum`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[v,x:T].    uiff(\muparrow{}bag-maximal?(\{v\};x;R);\muparrow{}(R  x  v))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``bag-maximal?  single-bag  bag-accum``  0  THEN  Auto)

---

Home Index