Step
*
1
of Lemma
EquatePairs-equality
1. x : Base
2. y : Base
3. n : Base
4. m : Base
5. ¬(y = n ∈ Base)
6. ¬(x = m ∈ Base)
7. ¬(n = m ∈ Base)
8. a : Base
9. b : Base
10. a = b ∈ EquatePairs(x;n;y;m)
⊢ ↓(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))))
BY
{ (Unfold `EquatePairs` -1 THEN At ⌜Type⌝ (PerElim (-1))⋅ THEN Try (Unhide) THEN Auto) }
Latex:
Latex:
1. x : Base
2. y : Base
3. n : Base
4. m : Base
5. \mneg{}(y = n)
6. \mneg{}(x = m)
7. \mneg{}(n = m)
8. a : Base
9. b : Base
10. a = b
\mvdash{} \mdownarrow{}(a = b)
\mvee{} (((x = a) \mwedge{} (n = b)) \mvee{} ((x = b) \mwedge{} (n = a)))
\mvee{} (((y = a) \mwedge{} (m = b)) \mvee{} ((y = b) \mwedge{} (m = a)))
\mvee{} ((x = y) \mwedge{} (((n = a) \mwedge{} (m = b)) \mvee{} ((n = b) \mwedge{} (m = a))))
By
Latex:
(Unfold `EquatePairs` -1 THEN At \mkleeneopen{}Type\mkleeneclose{} (PerElim (-1))\mcdot{} THEN Try (Unhide) THEN Auto)
Home
Index