---

Step * of Lemma fdl-eq-1

∀[X:Type]. ∀x:Point(free-dl(X)). (x = 1 ∈ Point(free-dl(X)) ⇐⇒ ↑fdl-is-1(x))
BY
{ (Intro⋅ THEN (Subst' Point(free-dl(X)) ~ free-dl-type(X) 0 THENA Computation) THEN (D 0 THENA Auto)) }

1
1. [X] : Type
2. x : free-dl-type(X)
⊢ x = 1 ∈ free-dl-type(X) ⇐⇒ ↑fdl-is-1(x)

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}x:Point(free-dl(X)).  (x  =  1  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}fdl-is-1(x))


By

---

Latex:
(Intro\mcdot{}  THEN  (Subst'  Point(free-dl(X))  \msim{}  free-dl-type(X)  0  THENA  Computation)  THEN  (D  0  THENA  Auto))

---

Home Index