---

Step * 1 1 1 1 of Lemma list_split_iseg


1. [T] : Type
2. f : (T List) ⟶ 𝔹
3. v1 : T List List
4. v2 : T List
5. v3 : T List List
6. v4 : T List
7. <v1, v2> = <v3, v4> ∈ (T List List × (T List))
⊢ ((v1 = v3 ∈ (T List List)) ∧ v2 ≤ v4)
∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v3 ∈ (T List List)) ∧ v2 ≤ Z))
BY
{ xxx(InstLemma `iseg_weakening` [] THEN OrLeft THEN Auto)xxx }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  (T  List)  {}\mrightarrow{}  \mBbbB{}
3.  v1  :  T  List  List
4.  v2  :  T  List
5.  v3  :  T  List  List
6.  v4  :  T  List
7.  <v1,  v2>  =  <v3,  v4>
\mvdash{}  ((v1  =  v3)  \mwedge{}  v2  \mleq{}  v4)  \mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:T  List  List.  (((v1  @  [Z  /  ZZ])  =  v3)  \mwedge{}  v2  \mleq{}  Z))


By

---

Latex:
xxx(InstLemma  `iseg\_weakening`  []  THEN  OrLeft  THEN  Auto)xxx

---

Home Index