---

Step * of Lemma first_index_equal

∀[T:Type]. ∀[L1,L2:T List]. ∀[P,Q:T ⟶ 𝔹].
  index-of-first a in L1.P[a] ∧b Q[a] = index-of-first a in L2.P[a] ∧b Q[a] ∈ ℤ supposing L1 agree_on(T;a.↑P[a]) L2
BY
{ (RepeatFor 2 (InductionOnList)
   THEN Unfold `agree_on` 0
   THEN (Auto THEN RepUR ``infix_ap`` (-1)⋅)
   THEN (D -1 THEN Auto' THEN (RW (SweepDnC FirstIndexC) 0 THENA Auto))⋅) }

1
1. T : Type
2. u : T
3. v : T List
4. ∀[L2:T List]. ∀[P,Q:T ⟶ 𝔹].
     index-of-first a in v.P[a] ∧b Q[a] = index-of-first a in L2.P[a] ∧b Q[a] ∈ ℤ supposing v agree_on(T;a.↑P[a]) L2
5. u1 : T
6. v1 : T List
7. ∀[P,Q:T ⟶ 𝔹].
     index-of-first a in [u / v].P[a] ∧b Q[a] = index-of-first a in v1.P[a] ∧b Q[a] ∈ ℤ 
     supposing [u / v] agree_on(T;a.↑P[a]) v1
8. P : T ⟶ 𝔹
9. Q : T ⟶ 𝔹
10. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
11. ∀i:ℕ||v|| + 1. (((↑P[[u / v][i]]) ∨ (↑P[[u1 / v1][i]])) ⇒ ([u / v][i] = [u1 / v1][i] ∈ T))
⊢ if P[u] ∧b Q[u] then 1
if 0 <z index-of-first a in v.P[a] ∧b Q[a] then index-of-first a in v.P[a] ∧b Q[a] + 1
else 0
fi 
= if P[u1] ∧b Q[u1] then 1
  if 0 <z index-of-first a in v1.P[a] ∧b Q[a] then index-of-first a in v1.P[a] ∧b Q[a] + 1
  else 0
  fi 
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L1,L2:T  List].  \mforall{}[P,Q:T  {}\mrightarrow{}  \mBbbB{}].
    index-of-first  a  in  L1.P[a]  \mwedge{}\msubb{}  Q[a]  =  index-of-first  a  in  L2.P[a]  \mwedge{}\msubb{}  Q[a] 
    supposing  L1  agree\_on(T;a.\muparrow{}P[a])  L2


By

---

Latex:
(RepeatFor  2  (InductionOnList)
  THEN  Unfold  `agree\_on`  0
  THEN  (Auto  THEN  RepUR  ``infix\_ap``  (-1)\mcdot{})
  THEN  (D  -1  THEN  Auto'  THEN  (RW  (SweepDnC  FirstIndexC)  0  THENA  Auto))\mcdot{})

---

Home Index