---

Step * of Lemma in-bar-equal

∀[T:Type]. ∀x:bar-base(T). ∀b:T.  (bar-equal(T;x;in-bar(b)) ⇐⇒ x↓b)
BY
{ Auto }

1
1. [T] : Type
2. x : bar-base(T)
3. b : T
4. bar-equal(T;x;in-bar(b))
⊢ x↓b

2
1. [T] : Type
2. x : bar-base(T)
3. b : T
4. x↓b
⊢ bar-equal(T;x;in-bar(b))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:bar-base(T).  \mforall{}b:T.    (bar-equal(T;x;in-bar(b))  \mLeftarrow{}{}\mRightarrow{}  x\mdownarrow{}b)


By

---

Latex:
Auto

---

Home Index