---

Step * of Lemma flattice-equiv-equiv

∀[X:Type]. EquivRel(Point(free-dl(X + X));x,y.flattice-equiv(X;x;y))
BY
{ (Intro
   THEN (Assert ((X + X) List List) ⊆r Point(free-dl(X + X)) BY
               ((Subst' Point(free-dl(X + X)) ~ free-dl-type(X + X) 0 THENA Computation) THEN Auto))
   THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
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)

2
1. X : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. a : Point(free-dl(X + X))
4. b : Point(free-dl(X + X))
5. flattice-equiv(X;a;b)
⊢ flattice-equiv(X;b;a)

3
1. X : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. Sym(Point(free-dl(X + X));x,y.flattice-equiv(X;x;y))
4. a : Point(free-dl(X + X))
5. b : Point(free-dl(X + X))
6. c : Point(free-dl(X + X))
7. flattice-equiv(X;a;b)
8. flattice-equiv(X;b;c)
⊢ flattice-equiv(X;a;c)

---

Latex:

---

Latex:
\mforall{}[X:Type].  EquivRel(Point(free-dl(X  +  X));x,y.flattice-equiv(X;x;y))


By

---

Latex:
(Intro
  THEN  (Assert  ((X  +  X)  List  List)  \msubseteq{}r  Point(free-dl(X  +  X))  BY
                          ((Subst'  Point(free-dl(X  +  X))  \msim{}  free-dl-type(X  +  X)  0  THENA  Computation)  THEN  Auto))
  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index