---

Step * 1 of Lemma flattice-equiv-equiv


1. [X] : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. a : Point(free-dl(X + X))
⊢ flattice-equiv(X;a;a)
BY
{ (UseWitness ⌜Ax⌝⋅
   THEN (Subst' Point(free-dl(X + X)) ~ free-dl-type(X + X) -1 THENA Computation)
   THEN (QuotientElimForEquality (-1) THENA Auto)
   THEN (Fold `member` 0 ORELSE ((Subst' Point(free-dl(X + X)) ~ free-dl-type(X + X) 0 THENA Computation) THEN Auto))) }

1
1. X : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. a : Base
4. a1 : Base
5. a = a1 ∈ pertype(λas,bs. ((as ∈ (X + X) List List) ∧ (bs ∈ (X + X) List List) ∧ dlattice-eq(X + X;as;bs)))
6. a ∈ (X + X) List List
7. a1 ∈ (X + X) List List
8. dlattice-eq(X + X;a;a1)
⊢ Ax ∈ flattice-equiv(X;a;a)

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  ((X  +  X)  List  List)  \msubseteq{}r  Point(free-dl(X  +  X))
3.  a  :  Point(free-dl(X  +  X))
\mvdash{}  flattice-equiv(X;a;a)


By

---

Latex:
(UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  (Subst'  Point(free-dl(X  +  X))  \msim{}  free-dl-type(X  +  X)  -1  THENA  Computation)
  THEN  (QuotientElimForEquality  (-1)  THENA  Auto)
  THEN  (Fold  `member`  0
  ORELSE  ((Subst'  Point(free-dl(X  +  X))  \msim{}  free-dl-type(X  +  X)  0  THENA  Computation)  THEN  Auto)
  ))

---

Home Index