---

Step * 1 1 of Lemma sqntype_list

.....assertion..... 
1. A : Type
2. n : ℕ
3. ∀x,y:Base.  ((x = y ∈ A) ⇒ (x ~n y))
⊢ ∀k:ℕ. ∀x,y:Base.  ((x = y ∈ (A List)) ⇒ (||x|| = k ∈ ℤ) ⇒ (x ~n y))
BY
{ (InductionOnNat THEN Intros) }

1
1. A : Type
2. n : ℕ
3. ∀x,y:Base.  ((x = y ∈ A) ⇒ (x ~n y))
4. k : ℤ
5. x : Base
6. y : Base
7. x = y ∈ (A List)
8. ||x|| = 0 ∈ ℤ
⊢ x ~n y

2
1. A : Type
2. n : ℕ
3. ∀x,y:Base.  ((x = y ∈ A) ⇒ (x ~n y))
4. k : ℤ
5. 0 < k
6. ∀x,y:Base.  ((x = y ∈ (A List)) ⇒ (||x|| = (k - 1) ∈ ℤ) ⇒ (x ~n y))
7. x : Base
8. y : Base
9. x = y ∈ (A List)
10. ||x|| = k ∈ ℤ
⊢ x ~n y

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  n  :  \mBbbN{}
3.  \mforall{}x,y:Base.    ((x  =  y)  {}\mRightarrow{}  (x  \msim{}n  y))
\mvdash{}  \mforall{}k:\mBbbN{}.  \mforall{}x,y:Base.    ((x  =  y)  {}\mRightarrow{}  (||x||  =  k)  {}\mRightarrow{}  (x  \msim{}n  y))


By

---

Latex:
(InductionOnNat  THEN  Intros)

---

Home Index