---

Step * of Lemma EquatePairs_wf

∀[x,y,n,m:Base].
  (EquatePairs(x;n;y;m) ∈ Type) supposing ((¬(n = m ∈ Base)) and (¬(x = m ∈ Base)) and (¬(y = n ∈ Base)))
BY
{ (Auto THEN Unfold `EquatePairs` 0 THEN At ⌜Type⌝ MemCD⋅) }

1
.....subterm..... T:t
1:n
1. x : Base
2. y : Base
3. n : Base
4. m : Base
5. ¬(y = n ∈ Base)
6. ¬(x = m ∈ Base)
7. ¬(n = m ∈ Base)
⊢ λa,b. ((a = b ∈ Base)
       ∨ (((x = a ∈ Base) ∧ (n = b ∈ Base)) ∨ ((x = b ∈ Base) ∧ (n = a ∈ Base)))
       ∨ (((y = a ∈ Base) ∧ (m = b ∈ Base)) ∨ ((y = b ∈ Base) ∧ (m = a ∈ Base)))
       ∨ ((x = y ∈ Base) ∧ (((n = a ∈ Base) ∧ (m = b ∈ Base)) ∨ ((n = b ∈ Base) ∧ (m = a ∈ Base))))) ∈ Base ⟶ Base ⟶ ℙ

2
1. x : Base
2. y : Base
3. n : Base
4. m : Base
5. ¬(y = n ∈ Base)
6. ¬(x = m ∈ Base)
7. ¬(n = m ∈ Base)
⊢ ∀x1,y1,z:Base.
    (((x1 = y1 ∈ Base)
     ∨ (((x = x1 ∈ Base) ∧ (n = y1 ∈ Base)) ∨ ((x = y1 ∈ Base) ∧ (n = x1 ∈ Base)))
     ∨ (((y = x1 ∈ Base) ∧ (m = y1 ∈ Base)) ∨ ((y = y1 ∈ Base) ∧ (m = x1 ∈ Base)))
     ∨ ((x = y ∈ Base) ∧ (((n = x1 ∈ Base) ∧ (m = y1 ∈ Base)) ∨ ((n = y1 ∈ Base) ∧ (m = x1 ∈ Base)))))
    ⇒ ((y1 = z ∈ Base)
       ∨ (((x = y1 ∈ Base) ∧ (n = z ∈ Base)) ∨ ((x = z ∈ Base) ∧ (n = y1 ∈ Base)))
       ∨ (((y = y1 ∈ Base) ∧ (m = z ∈ Base)) ∨ ((y = z ∈ Base) ∧ (m = y1 ∈ Base)))
       ∨ ((x = y ∈ Base) ∧ (((n = y1 ∈ Base) ∧ (m = z ∈ Base)) ∨ ((n = z ∈ Base) ∧ (m = y1 ∈ Base)))))
    ⇒ ((x1 = z ∈ Base)
       ∨ (((x = x1 ∈ Base) ∧ (n = z ∈ Base)) ∨ ((x = z ∈ Base) ∧ (n = x1 ∈ Base)))
       ∨ (((y = x1 ∈ Base) ∧ (m = z ∈ Base)) ∨ ((y = z ∈ Base) ∧ (m = x1 ∈ Base)))
       ∨ ((x = y ∈ Base) ∧ (((n = x1 ∈ Base) ∧ (m = z ∈ Base)) ∨ ((n = z ∈ Base) ∧ (m = x1 ∈ Base))))))

3
1. x : Base
2. y : Base
3. n : Base
4. m : Base
5. ¬(y = n ∈ Base)
6. ¬(x = m ∈ Base)
7. ¬(n = m ∈ Base)
⊢ ∀x1,y1:Base.
    (((x1 = y1 ∈ Base)
    ∨ (((x = x1 ∈ Base) ∧ (n = y1 ∈ Base)) ∨ ((x = y1 ∈ Base) ∧ (n = x1 ∈ Base)))
    ∨ (((y = x1 ∈ Base) ∧ (m = y1 ∈ Base)) ∨ ((y = y1 ∈ Base) ∧ (m = x1 ∈ Base)))
    ∨ ((x = y ∈ Base) ∧ (((n = x1 ∈ Base) ∧ (m = y1 ∈ Base)) ∨ ((n = y1 ∈ Base) ∧ (m = x1 ∈ Base)))))
    ⇒ ((y1 = x1 ∈ Base)
       ∨ (((x = y1 ∈ Base) ∧ (n = x1 ∈ Base)) ∨ ((x = x1 ∈ Base) ∧ (n = y1 ∈ Base)))
       ∨ (((y = y1 ∈ Base) ∧ (m = x1 ∈ Base)) ∨ ((y = x1 ∈ Base) ∧ (m = y1 ∈ Base)))
       ∨ ((x = y ∈ Base) ∧ (((n = y1 ∈ Base) ∧ (m = x1 ∈ Base)) ∨ ((n = x1 ∈ Base) ∧ (m = y1 ∈ Base))))))

---

Latex:

---

Latex:
\mforall{}[x,y,n,m:Base].    (EquatePairs(x;n;y;m)  \mmember{}  Type)  supposing  ((\mneg{}(n  =  m))  and  (\mneg{}(x  =  m))  and  (\mneg{}(y  =  n)))


By

---

Latex:
(Auto  THEN  Unfold  `EquatePairs`  0  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  MemCD\mcdot{})

---

Home Index