---

Step * of Lemma cons-proper-iseg

∀[T:Type]. ∀L1,L2:T List. ∀a,b:T.  ([a / L1] < [b / L2] ⇐⇒ L1 < L2 ∧ (a = b ∈ T))
BY
{ (Unfold `proper-iseg` 0
   THEN (UnivCD THENA Auto)
   THEN RWO "cons_iseg" 0
   THEN Auto
   THEN OnMaybeHyp 8 (\h. (ParallelOp h THEN Auto))⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2:T  List.  \mforall{}a,b:T.    ([a  /  L1]  <  [b  /  L2]  \mLeftarrow{}{}\mRightarrow{}  L1  <  L2  \mwedge{}  (a  =  b))


By

---

Latex:
(Unfold  `proper-iseg`  0
  THEN  (UnivCD  THENA  Auto)
  THEN  RWO  "cons\_iseg"  0
  THEN  Auto
  THEN  OnMaybeHyp  8  (\mbackslash{}h.  (ParallelOp  h  THEN  Auto))\mcdot{})

---

Home Index