---

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


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, v3> = <v4, v5> ∈ (ℤ × A)@i
⊢ <v2, v3> = <v4, v5> ∈ (T × A)
BY
{ ((EqHD (-1) THEN Auto) THEN EqCD THEN Auto) }

1
.....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

---

Latex:

---

Latex:

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.  <v2,  v3>  =  <v4,  v5>@i
\mvdash{}  <v2,  v3>  =  <v4,  v5>


By

---

Latex:
((EqHD  (-1)  THEN  Auto)  THEN  EqCD  THEN  Auto)

---

Home Index