Step
*
3
of Lemma
assoced_nelim
.....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 ∈ ℤ)
BY
{ (GenRepD THENA Auto) }
Latex:
Latex:
.....wf.....
1. a : \mBbbN{}
2. b : \mBbbN{}
3. ((a = b) \mvee{} (a = (-b))) {}\mRightarrow{} (a = b)
4. (a \msim{} b) {}\mRightarrow{} (a = b)
5. ((a = b) \mvee{} (a = (-b))) \mLeftarrow{}{} a = b
\mvdash{} istype(a = b)
By
Latex:
(GenRepD THENA Auto)
Home
Index