---

Step * of Lemma assert-deq-all-disjoint

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[ass:A List List]. ∀[bs:A List].
  uiff(↑deq-all-disjoint(eq;ass;bs);(∀as∈ass.l_disjoint(A;as;bs)))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `deq-all-disjoint` 0
   THEN RW assert_pushdownC 0
   THEN Auto
   THEN RepeatFor 3 (ParallelLast)) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[ass:A  List  List].  \mforall{}[bs:A  List].
    uiff(\muparrow{}deq-all-disjoint(eq;ass;bs);(\mforall{}as\mmember{}ass.l\_disjoint(A;as;bs)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `deq-all-disjoint`  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto
  THEN  RepeatFor  3  (ParallelLast))

---

Home Index