---

Step * of Lemma sqn+1type_dep_product

∀[T:Type]. ∀[S:T ⟶ Type]. ∀[n:ℕ].  (sqntype(n + 1;t:T × S[t])) supposing ((∀t:T. sqntype(n;S[t])) and sqntype(n;T))
BY
{ (Auto
   THEN All (Unfold `sqntype`)
   THEN Auto
   THEN UseWitness ⌜Ax⌝⋅
   THEN Unfold `member` 0
   THEN Refine `axiomSqequalN` []
   THEN All (Unfold `sqntype`)) }

1
1. T : Type
2. S : T ⟶ Type
3. n : ℕ
4. ∀x,y:Base.  ((x = y ∈ T) ⇒ (x ~n y))
5. ∀t:T. ∀x,y:Base.  ((x = y ∈ S[t]) ⇒ (x ~n y))
6. x : Base
7. y : Base
8. x = y ∈ (t:T × S[t])
⊢ x ~n + 1 y

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  All  (Unfold  `sqntype`)
  THEN  Auto
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  Unfold  `member`  0
  THEN  Refine  `axiomSqequalN`  []
  THEN  All  (Unfold  `sqntype`))

---

Home Index