---

Step * of Lemma exists-type-equating-ints

∀x,y,n,m:ℤ.
  ((¬(x = y ∈ ℤ))
  ⇒ (¬(n = m ∈ ℤ))
  ⇒ (¬(x = m ∈ ℤ))
  ⇒ (¬(y = n ∈ ℤ))
  ⇒ (∃T:Type. ((x = n ∈ T) ∧ (y = m ∈ T) ∧ (¬(x = y ∈ T)))))
BY
{ (Auto
   THEN ((InstLemma `type-equating-some` [⌜ℤ⌝;⌜λ2z.(z = x ∈ ℤ) ∨ (z = n ∈ ℤ)⌝]⋅ THENA Auto) THEN ExRepD)
   THEN (InstLemma `type-equating-some` [⌜T'⌝;⌜λ2z.(z = y ∈ T') ∨ (z = m ∈ T')⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN RenameVar `T' (-4)
   THEN D 0 With ⌜T⌝ 
   THEN Auto) }

1
1. x : ℤ
2. y : ℤ
3. n : ℤ
4. m : ℤ
5. ¬(x = y ∈ ℤ)
6. ¬(n = m ∈ ℤ)
7. ¬(x = m ∈ ℤ)
8. ¬(y = n ∈ ℤ)
9. T' : Type
10. ℤ ⊆r T'
11. ∀x@0,y:ℤ.  (((x@0 = x ∈ ℤ) ∨ (x@0 = n ∈ ℤ)) ⇒ ((y = x ∈ ℤ) ∨ (y = n ∈ ℤ)) ⇒ (x@0 = y ∈ T'))
12. ∀x@0,y:ℤ.  ((¬((x@0 = x ∈ ℤ) ∨ (x@0 = n ∈ ℤ))) ⇒ (x@0 = y ∈ ℤ ⇐⇒ x@0 = y ∈ T'))
13. T : Type
14. T' ⊆r T
15. ∀x,y@0:T'.  (((x = y ∈ T') ∨ (x = m ∈ T')) ⇒ ((y@0 = y ∈ T') ∨ (y@0 = m ∈ T')) ⇒ (x = y@0 ∈ T))
16. ∀x,y@0:T'.  ((¬((x = y ∈ T') ∨ (x = m ∈ T'))) ⇒ (x = y@0 ∈ T' ⇐⇒ x = y@0 ∈ T))
⊢ x = n ∈ T

2
1. x : ℤ
2. y : ℤ
3. n : ℤ
4. m : ℤ
5. ¬(x = y ∈ ℤ)
6. ¬(n = m ∈ ℤ)
7. ¬(x = m ∈ ℤ)
8. ¬(y = n ∈ ℤ)
9. T' : Type
10. ℤ ⊆r T'
11. ∀x@0,y:ℤ.  (((x@0 = x ∈ ℤ) ∨ (x@0 = n ∈ ℤ)) ⇒ ((y = x ∈ ℤ) ∨ (y = n ∈ ℤ)) ⇒ (x@0 = y ∈ T'))
12. ∀x@0,y:ℤ.  ((¬((x@0 = x ∈ ℤ) ∨ (x@0 = n ∈ ℤ))) ⇒ (x@0 = y ∈ ℤ ⇐⇒ x@0 = y ∈ T'))
13. T : Type
14. T' ⊆r T
15. ∀x,y@0:T'.  (((x = y ∈ T') ∨ (x = m ∈ T')) ⇒ ((y@0 = y ∈ T') ∨ (y@0 = m ∈ T')) ⇒ (x = y@0 ∈ T))
16. ∀x,y@0:T'.  ((¬((x = y ∈ T') ∨ (x = m ∈ T'))) ⇒ (x = y@0 ∈ T' ⇐⇒ x = y@0 ∈ T))
17. x = n ∈ T
18. y = m ∈ T
⊢ ¬(x = y ∈ T)

---

Latex:

---

Latex:
\mforall{}x,y,n,m:\mBbbZ{}.
    ((\mneg{}(x  =  y))
    {}\mRightarrow{}  (\mneg{}(n  =  m))
    {}\mRightarrow{}  (\mneg{}(x  =  m))
    {}\mRightarrow{}  (\mneg{}(y  =  n))
    {}\mRightarrow{}  (\mexists{}T:Type.  ((x  =  n)  \mwedge{}  (y  =  m)  \mwedge{}  (\mneg{}(x  =  y)))))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `type-equating-some`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}z.(z  =  x)  \mvee{}  (z  =  n)\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (InstLemma  `type-equating-some`  [\mkleeneopen{}T'\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}z.(z  =  y)  \mvee{}  (z  =  m)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  RenameVar  `T'  (-4)
  THEN  D  0  With  \mkleeneopen{}T\mkleeneclose{} 
  THEN  Auto)

---

Home Index