---

Step * 2 of Lemma proper-iseg-append


1. T : Type
2. u : T
3. v : T List
4. ∀L2,L3,L4:T List.  v @ L3 < L2 @ L4 ⇐⇒ L3 < L4 ∧ (v = L2 ∈ (T List)) supposing ||v|| = ||L2|| ∈ ℤ
5. u1 : T
6. v1 : T List
7. ∀L3,L4:T List.  [u / v] @ L3 < v1 @ L4 ⇐⇒ L3 < L4 ∧ ([u / v] = v1 ∈ (T List)) supposing ||[u / v]|| = ||v1|| ∈ ℤ
8. L3 : T List
9. L4 : T List
10. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
11. [u / (v @ L3)] < [u1 / (v1 @ L4)]
⊢ [u / v] = [u1 / v1] ∈ (T List)
BY
{ ((RWO "cons-proper-iseg" (-1) THENA Auto) THEN EqCD THEN Auto THEN InstHyp [⌜v1⌝;⌜L3⌝;⌜L4⌝] 4⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}L2,L3,L4:T  List.    v  @  L3  <  L2  @  L4  \mLeftarrow{}{}\mRightarrow{}  L3  <  L4  \mwedge{}  (v  =  L2)  supposing  ||v||  =  ||L2||
5.  u1  :  T
6.  v1  :  T  List
7.  \mforall{}L3,L4:T  List.
          [u  /  v]  @  L3  <  v1  @  L4  \mLeftarrow{}{}\mRightarrow{}  L3  <  L4  \mwedge{}  ([u  /  v]  =  v1)  supposing  ||[u  /  v]||  =  ||v1||
8.  L3  :  T  List
9.  L4  :  T  List
10.  (||v||  +  1)  =  (||v1||  +  1)
11.  [u  /  (v  @  L3)]  <  [u1  /  (v1  @  L4)]
\mvdash{}  [u  /  v]  =  [u1  /  v1]


By

---

Latex:
((RWO  "cons-proper-iseg"  (-1)  THENA  Auto)
  THEN  EqCD
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}L3\mkleeneclose{};\mkleeneopen{}L4\mkleeneclose{}]  4\mcdot{}
  THEN  Auto)

---

Home Index