---

Step * of Lemma sqntype_product

∀[T,S:Type]. ∀[n:ℕ].  (sqntype(n;T × S)) supposing (sqntype(n;S) and sqntype(n;T))
BY
{ (InstLemma `sqn+1type_product` [] THEN RepeatFor 9 (ParallelLast') THEN Auto) }

1
1. [T] : Type
2. [S] : Type
3. [n] : ℕ
4. [%1] : 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

---

Latex:

---

Latex:
\mforall{}[T,S:Type].  \mforall{}[n:\mBbbN{}].    (sqntype(n;T  \mtimes{}  S))  supposing  (sqntype(n;S)  and  sqntype(n;T))


By

---

Latex:
(InstLemma  `sqn+1type\_product`  []  THEN  RepeatFor  9  (ParallelLast')  THEN  Auto)

---

Home Index