---

Step * 1 of Lemma l_disjoint_singleton


1. T : Type
2. a : T List
3. x : T
4. ∀x@0:T. (¬((x@0 ∈ a) ∧ (x@0 = x ∈ T)))
⊢ ¬(x ∈ a)
BY
{ TACTIC:((InstHyp [⌜x⌝] (-1))⋅ THEN Auto THEN ParallelLast THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  a  :  T  List
3.  x  :  T
4.  \mforall{}x@0:T.  (\mneg{}((x@0  \mmember{}  a)  \mwedge{}  (x@0  =  x)))
\mvdash{}  \mneg{}(x  \mmember{}  a)


By

---

Latex:
TACTIC:((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1))\mcdot{}  THEN  Auto  THEN  ParallelLast  THEN  Auto)

---

Home Index