---

Step * of Lemma assert-deq-disjoint

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[as,bs:A List].  uiff(↑deq-disjoint(eq;as;bs);l_disjoint(A;as;bs))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `deq-disjoint` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (RWO "l_all_iff" 0 THENA Auto)
   THEN Unfold `l_disjoint` 0
   THEN Auto
   THEN D 0
   THEN Auto
   THEN (With ⌜a⌝ (D (-4))⋅ THENM D -1)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `deq-disjoint`  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (RWO  "l\_all\_iff"  0  THENA  Auto)
  THEN  Unfold  `l\_disjoint`  0
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  (With  \mkleeneopen{}a\mkleeneclose{}  (D  (-4))\mcdot{}  THENM  D  -1)
  THEN  Auto)

---

Home Index