---

Step * 2 1 1 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 = v4 ∈ ℤ
9. v3 = v5 ∈ A
⊢ v2 = v4 ∈ T
BY
{ (HypSubst' (-2) 0 THEN Auto)⋅ }

---

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


By

---

Latex:
(HypSubst'  (-2)  0  THEN  Auto)\mcdot{}

---

Home Index