---

Step * of Lemma poss-maj-member

∀T:Type. ∀eq:EqDecider(T). ∀L:T List. ∀x:T.  (snd(poss-maj(eq;L;x)) ∈ [x / L])
BY
{ (UnivCD THENA Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
⊢ (snd(poss-maj(eq;L;x)) ∈ [x / L])

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}x:T.    (snd(poss-maj(eq;L;x))  \mmember{}  [x  /  L])


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index