---

Step * 1 of Lemma sqn+1type_dep_product


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
BY
{ ((Subst' x ~ <fst(x), snd(x)> 0 THENA ((GenConcl ⌜x = X ∈ (t:T × S[t])⌝⋅ THENA Auto) THEN DProds THEN Reduce 0 THEN Au\000Cto))
   THEN (Subst' y ~ <fst(y), snd(y)> 0 THENA ((GenConcl ⌜y = X ∈ (t:T × S[t])⌝⋅ THENA Auto) THEN DProds THEN Reduce 0 TH\000CEN Auto))
   THEN (EqHD (-1) THENA Auto)
   THEN SqequalNCanonicalCD
   THEN Subst' (n + 1) - 1 ~ n 0
   THEN Auto) }

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. (fst(x)) = (fst(y)) ∈ T
9. (snd(x)) = (snd(y)) ∈ S[fst(x)]
10. 0 < n + 1
⊢ snd(x) ~n snd(y)

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  T  {}\mrightarrow{}  Type
3.  n  :  \mBbbN{}
4.  \mforall{}x,y:Base.    ((x  =  y)  {}\mRightarrow{}  (x  \msim{}n  y))
5.  \mforall{}t:T.  \mforall{}x,y:Base.    ((x  =  y)  {}\mRightarrow{}  (x  \msim{}n  y))
6.  x  :  Base
7.  y  :  Base
8.  x  =  y
\mvdash{}  x  \msim{}n  +  1  y


By

---

Latex:
((Subst'  x  \msim{}  <fst(x),  snd(x)>  0  THENA  ((GenConcl  \mkleeneopen{}x  =  X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  DProds  THEN  Reduce  0  THEN\000C  Auto))
  THEN  (Subst'  y  \msim{}  <fst(y),  snd(y)>  0
              THENA  ((GenConcl  \mkleeneopen{}y  =  X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  DProds  THEN  Reduce  0  THEN  Auto)
              )
  THEN  (EqHD  (-1)  THENA  Auto)
  THEN  SqequalNCanonicalCD
  THEN  Subst'  (n  +  1)  -  1  \msim{}  n  0
  THEN  Auto)

---

Home Index