---

Step * of Lemma implies-bar-equal

∀[T:Type]. ∀x,y:bar-base(T).  (((∃a:T. (x↓a ∧ y↓a)) ∨ (x↑ ∧ y↑)) ⇒ bar-equal(T;x;y))
BY
{ (Auto THEN D -1 THEN ExRepD) }

1
1. [T] : Type
2. x : bar-base(T)@i
3. y : bar-base(T)@i
4. a : T@i
5. x↓a
6. y↓a
⊢ bar-equal(T;x;y)

2
1. [T] : Type
2. x : bar-base(T)@i
3. y : bar-base(T)@i
4. x↑
5. y↑
⊢ bar-equal(T;x;y)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x,y:bar-base(T).    (((\mexists{}a:T.  (x\mdownarrow{}a  \mwedge{}  y\mdownarrow{}a))  \mvee{}  (x\muparrow{}  \mwedge{}  y\muparrow{}))  {}\mRightarrow{}  bar-equal(T;x;y))


By

---

Latex:
(Auto  THEN  D  -1  THEN  ExRepD)

---

Home Index