---

Step * 1 of Lemma fdl-eq-1


1. [X] : Type
2. x : free-dl-type(X)@i
⊢ x = 1 ∈ free-dl-type(X) ⇐⇒ ↑fdl-is-1(x)
BY
{ (UseWitness ⌜<λx.Ax, λx.Ax>⌝⋅ THEN (QuotientElimForEquality (-1) THENA Auto)) }

1
1. X : Type
2. x : as,bs:X List List//dlattice-eq(X;as;bs)
⊢ fdl-is-1(x) ∈ 𝔹

2
1. X : Type
2. x : Base
3. x1 : Base
4. x = x1 ∈ pertype(λas,bs. ((as ∈ X List List) ∧ (bs ∈ X List List) ∧ dlattice-eq(X;as;bs)))
5. x ∈ X List List
6. x1 ∈ X List List
7. dlattice-eq(X;x;x1)
⊢ <λx.Ax, λx.Ax> = <λx.Ax, λx.Ax> ∈ (x = 1 ∈ free-dl-type(X) ⇐⇒ ↑fdl-is-1(x))

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  x  :  free-dl-type(X)@i
\mvdash{}  x  =  1  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}fdl-is-1(x)


By

---

Latex:
(UseWitness  \mkleeneopen{}<\mlambda{}x.Ax,  \mlambda{}x.Ax>\mkleeneclose{}\mcdot{}  THEN  (QuotientElimForEquality  (-1)  THENA  Auto))

---

Home Index