---

Step * 2 1 1 of Lemma agree_on_equiv


1. T : Type
2. P : T ⟶ ℙ
3. ∀a,b:T List.
     (((||a|| = ||b|| ∈ ℤ) c∧ (∀i:ℕ||a||. ((P[a[i]] ∨ P[b[i]]) ⇒ (a[i] = b[i] ∈ T))))
     ⇒ ((||b|| = ||a|| ∈ ℤ) c∧ (∀i:ℕ||b||. ((P[b[i]] ∨ P[a[i]]) ⇒ (b[i] = a[i] ∈ T)))))
4. a : T List
5. b : T List
6. c : T List
7. ||a|| = ||b|| ∈ ℤ
8. ∀i:ℕ||a||. ((P[a[i]] ∨ P[b[i]]) ⇒ (a[i] = b[i] ∈ T))
9. ||b|| = ||c|| ∈ ℤ
10. ∀i:ℕ||b||. ((P[b[i]] ∨ P[c[i]]) ⇒ (b[i] = c[i] ∈ T))
11. ||a|| = ||c|| ∈ ℤ
12. i : ℕ||a||
13. P[a[i]]
⊢ a[i] = c[i] ∈ T
BY
{ ((Assert a[i] = b[i] ∈ T BY Auto) THEN HypSubst (-1) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}a,b:T  List.
          (((||a||  =  ||b||)  c\mwedge{}  (\mforall{}i:\mBbbN{}||a||.  ((P[a[i]]  \mvee{}  P[b[i]])  {}\mRightarrow{}  (a[i]  =  b[i]))))
          {}\mRightarrow{}  ((||b||  =  ||a||)  c\mwedge{}  (\mforall{}i:\mBbbN{}||b||.  ((P[b[i]]  \mvee{}  P[a[i]])  {}\mRightarrow{}  (b[i]  =  a[i])))))
4.  a  :  T  List
5.  b  :  T  List
6.  c  :  T  List
7.  ||a||  =  ||b||
8.  \mforall{}i:\mBbbN{}||a||.  ((P[a[i]]  \mvee{}  P[b[i]])  {}\mRightarrow{}  (a[i]  =  b[i]))
9.  ||b||  =  ||c||
10.  \mforall{}i:\mBbbN{}||b||.  ((P[b[i]]  \mvee{}  P[c[i]])  {}\mRightarrow{}  (b[i]  =  c[i]))
11.  ||a||  =  ||c||
12.  i  :  \mBbbN{}||a||
13.  P[a[i]]
\mvdash{}  a[i]  =  c[i]


By

---

Latex:
((Assert  a[i]  =  b[i]  BY  Auto)  THEN  HypSubst  (-1)  0  THEN  Auto)

---

Home Index