---

Step * 1 of Lemma agree_on_equiv


1. T : Type
2. P : T ⟶ ℙ
3. a : T List
4. b : T List
5. (||a|| = ||b|| ∈ ℤ) c∧ (∀i:ℕ||a||. ((P[a[i]] ∨ P[b[i]]) ⇒ (a[i] = b[i] ∈ T)))
6. ||b|| = ||a|| ∈ ℤ
7. i : ℕ||b||
8. P[b[i]] ∨ P[a[i]]
⊢ b[i] = a[i] ∈ T
BY
{ (Symmetry THEN BackThruSomeHyp THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Symmetry  THEN  BackThruSomeHyp  THEN  D  -1  THEN  Auto)

---

Home Index