---

Step * 1 1 of Lemma sqntype_product


1. T : Type
2. S : Type
3. n : ℕ
4. sqntype(n;T)
5. sqntype(n;S)
6. x : Base@i
7. y : Base@i
8. x = y ∈ (T × S)
9. x ~n + 1 y
⊢ x ~n y
BY
{ (FLemma `sqequal_n_add` [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  Type
3.  n  :  \mBbbN{}
4.  sqntype(n;T)
5.  sqntype(n;S)
6.  x  :  Base@i
7.  y  :  Base@i
8.  x  =  y
9.  x  \msim{}n  +  1  y
\mvdash{}  x  \msim{}n  y


By

---

Latex:
(FLemma  `sqequal\_n\_add`  [-1]  THEN  Auto)

---

Home Index