---

Step * of Lemma hd-append

∀[T:Type]. ∀[L1:T List+]. ∀[L2:T List].  (hd(L1 @ L2) = hd(L1) ∈ T)
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "select-as-hd<" 0 THENA Auto)
   THEN D (-2)
   THEN (RWO "select_append" 0 THENA Auto')
   THEN Subst ⌜0 <z ||L1|| ~ tt⌝ 0⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L1:T  List\msupplus{}].  \mforall{}[L2:T  List].    (hd(L1  @  L2)  =  hd(L1))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "select-as-hd<"  0  THENA  Auto)
  THEN  D  (-2)
  THEN  (RWO  "select\_append"  0  THENA  Auto')
  THEN  Subst  \mkleeneopen{}0  <z  ||L1||  \msim{}  tt\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index