---

Step * of Lemma iseg-transition-lemma

∀[T:Type]. ∀[P:(T List) ⟶ ℙ].
  ∀L:T List. ∀x:T.
    ((∃L1:T List. (L1 ≤ L @ [x] ∧ P[L1])) ∧ (¬(∃L1:T List. (L1 ≤ L ∧ P[L1])))
    ⇐⇒ P[L @ [x]] ∧ (¬(∃L1:T List. (L1 ≤ L ∧ P[L1]))))
BY
{ Auto }

1
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. L : T List
4. x : T
5. ∃L1:T List. (L1 ≤ L @ [x] ∧ P[L1])
6. ¬(∃L1:T List. (L1 ≤ L ∧ P[L1]))
⊢ P[L @ [x]]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}L:T  List.  \mforall{}x:T.
        ((\mexists{}L1:T  List.  (L1  \mleq{}  L  @  [x]  \mwedge{}  P[L1]))  \mwedge{}  (\mneg{}(\mexists{}L1:T  List.  (L1  \mleq{}  L  \mwedge{}  P[L1])))
        \mLeftarrow{}{}\mRightarrow{}  P[L  @  [x]]  \mwedge{}  (\mneg{}(\mexists{}L1:T  List.  (L1  \mleq{}  L  \mwedge{}  P[L1]))))


By

---

Latex:
Auto

---

Home Index