---

Step * 2 1 1 1 1 1 of Lemma max-fst-property

.....subterm..... T:t
1:n
1. A : Type@i'
2. T : Type@i'
3. v2 : T@i
4. v3 : A@i
5. v4 : T@i
6. v5 : A@i
7. T ⊆r ℤ@i
8. (fst(<v2, v3>)) = (fst(<v4, v5>)) ∈ ℤ
9. (snd(<v2, v3>)) = (snd(<v4, v5>)) ∈ A
⊢ v2 = v4 ∈ T
BY
{ All Reduce }

1
1. A : Type@i'
2. T : Type@i'
3. v2 : T@i
4. v3 : A@i
5. v4 : T@i
6. v5 : A@i
7. T ⊆r ℤ@i
8. v2 = v4 ∈ ℤ
9. v3 = v5 ∈ A
⊢ v2 = v4 ∈ T

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  Type@i'
2.  T  :  Type@i'
3.  v2  :  T@i
4.  v3  :  A@i
5.  v4  :  T@i
6.  v5  :  A@i
7.  T  \msubseteq{}r  \mBbbZ{}@i
8.  (fst(<v2,  v3>))  =  (fst(<v4,  v5>))
9.  (snd(<v2,  v3>))  =  (snd(<v4,  v5>))
\mvdash{}  v2  =  v4


By

---

Latex:
All  Reduce

---

Home Index