Step
*
of Lemma
assoced_nelim
∀a,b:ℕ. (a ~ b
⇐⇒ a = b ∈ ℤ)
BY
{ ((RepD THENM RWH (LemmaC `assoced_elim`) 0) THENA Auto{1,3}-1) }
1
1. a : ℕ
2. b : ℕ
⊢ (a = b ∈ ℤ) ∨ (a = (-b) ∈ ℤ)
⇐⇒ a = b ∈ ℤ
2
.....wf.....
1. a : ℕ
2. b : ℕ
3. ((a = b ∈ ℤ) ∨ (a = (-b) ∈ ℤ))
⇒ (a = b ∈ ℤ)
⊢ istype(a ~ b)
3
.....wf.....
1. a : ℕ
2. b : ℕ
3. ((a = b ∈ ℤ) ∨ (a = (-b) ∈ ℤ))
⇒ (a = b ∈ ℤ)
4. (a ~ b)
⇒ (a = b ∈ ℤ)
5. ((a = b ∈ ℤ) ∨ (a = (-b) ∈ ℤ))
⇐ a = b ∈ ℤ
⊢ istype(a = b ∈ ℤ)
4
.....wf.....
1. a : ℕ
⊢ istype(ℕ)
5
.....wf.....
istype(ℕ)
Latex:
Latex:
\mforall{}a,b:\mBbbN{}. (a \msim{} b \mLeftarrow{}{}\mRightarrow{} a = b)
By
Latex:
((RepD THENM RWH (LemmaC `assoced\_elim`) 0) THENA Auto\{1,3\}-1)
Home
Index