---

Step * of Lemma l_disjoint_append2

∀[T:Type]. ∀[a,b,c:T List].  uiff(l_disjoint(T;b @ c;a);l_disjoint(T;b;a) ∧ l_disjoint(T;c;a))
BY
{ TACTIC:(Intros
          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 ∈ b) ∧ (x ∈ a)))
6. ∀x:T. (¬((x ∈ c) ∧ (x ∈ a)))
7. x : T
8. ¬((x ∈ c) ∧ (x ∈ a))
9. ¬((x ∈ b) ∧ (x ∈ a))
⊢ ¬(((x ∈ b) ∨ (x ∈ c)) ∧ (x ∈ a))

---

Latex:

---

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


By

---

Latex:
TACTIC:(Intros
                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