---

Step * 1 of Lemma sqntype_product


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
BY
{ (UseWitness ⌜Ax⌝⋅ THEN Unfold `member` 0 THEN Refine `axiomSqequalN` []) }

1
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

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [S]  :  Type
3.  [n]  :  \mBbbN{}
4.  [\%1]  :  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:
(UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  Unfold  `member`  0  THEN  Refine  `axiomSqequalN`  [])

---

Home Index