---

Step * of Lemma compat-common-member

∀[T:Type]. ∀[L1,L2:T List].  ∀[k:ℕ]. (L1[k] = L2[k] ∈ T) supposing (k < ||L2|| and k < ||L1||) supposing L1 || L2
BY
{ (Auto THEN RepeatFor 2 (D -4) THEN (HypSubst' (-4) 0 THEN Auto) THEN RWO "select_append_front" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L1,L2:T  List].    \mforall{}[k:\mBbbN{}].  (L1[k]  =  L2[k])  supposing  (k  <  ||L2||  and  k  <  ||L1||)  supposing\000C  L1  ||  L2


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -4)
  THEN  (HypSubst'  (-4)  0  THEN  Auto)
  THEN  RWO  "select\_append\_front"  0
  THEN  Auto)

---

Home Index