---

Step * of Lemma l_disjoint_append

∀[T:Type]. ∀[a,b,c:T List].  uiff(l_disjoint(T;a;b @ c);l_disjoint(T;a;b) ∧ l_disjoint(T;a;c))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN Unfold `l_disjoint` 0
          THEN RWO "member_append" 0
          THEN Auto
          THEN ∀h:hyp. ((InstHyp [⌜x⌝] h)⋅ THEN Auto) ) }

1
1. T : Type
2. a : T List
3. b : T List
4. c : T List
5. ∀x:T. (¬((x ∈ a) ∧ (x ∈ b)))
6. ∀x:T. (¬((x ∈ a) ∧ (x ∈ c)))
7. x : T
8. ¬((x ∈ a) ∧ (x ∈ c))
9. ¬((x ∈ a) ∧ (x ∈ b))
⊢ ¬((x ∈ a) ∧ ((x ∈ b) ∨ (x ∈ c)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a,b,c:T  List].    uiff(l\_disjoint(T;a;b  @  c);l\_disjoint(T;a;b)  \mwedge{}  l\_disjoint(T;a;c))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  Unfold  `l\_disjoint`  0
                THEN  RWO  "member\_append"  0
                THEN  Auto
                THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h)\mcdot{}  THEN  Auto)  )

---

Home Index