---

Step * 1 1 of Lemma pairwise-implies


1. T : Type
2. L : T List
3. P : T ⟶ T ⟶ ℙ'
4. ∀i:ℕ||L||. ∀j:ℕi.  P[L[j];L[i]]
5. x : T
6. y : T
7. i1 : ℕ
8. i1 < ||L||
9. x = L[i1] ∈ T
10. i : ℕ
11. i < ||L||
12. y = L[i] ∈ T
13. ¬i1 < i
14. ¬i < i1
⊢ L[i1] = L[i] ∈ T
BY
{ (EqCD THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  P  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}'
4.  \mforall{}i:\mBbbN{}||L||.  \mforall{}j:\mBbbN{}i.    P[L[j];L[i]]
5.  x  :  T
6.  y  :  T
7.  i1  :  \mBbbN{}
8.  i1  <  ||L||
9.  x  =  L[i1]
10.  i  :  \mBbbN{}
11.  i  <  ||L||
12.  y  =  L[i]
13.  \mneg{}i1  <  i
14.  \mneg{}i  <  i1
\mvdash{}  L[i1]  =  L[i]


By

---

Latex:
(EqCD  THEN  Auto')\mcdot{}

---

Home Index