---

Step * of Lemma agree_on_equiv

∀[T:Type]. ∀[P:T ⟶ ℙ].  EquivRel(T List)(_1 agree_on(T;a.P[a]) _2)
BY
{ (Auto THEN D 0 THEN RepUR ``refl sym trans agree_on`` 0 THEN Auto) }

1
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

2
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|| ∈ ℤ) c∧ (∀i:ℕ||a||. ((P[a[i]] ∨ P[b[i]]) ⇒ (a[i] = b[i] ∈ T)))
8. (||b|| = ||c|| ∈ ℤ) c∧ (∀i:ℕ||b||. ((P[b[i]] ∨ P[c[i]]) ⇒ (b[i] = c[i] ∈ T)))
9. ||a|| = ||c|| ∈ ℤ
10. i : ℕ||a||
11. P[a[i]] ∨ P[c[i]]
⊢ a[i] = c[i] ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    EquivRel(T  List)($_{1}$  agree\_on(T;a.P[a])  $_\mbackslash{}f\000Cf7b2}$)


By

---

Latex:
(Auto  THEN  D  0  THEN  RepUR  ``refl  sym  trans  agree\_on``  0  THEN  Auto)

---

Home Index