---

Step * 1 2 of Lemma fdl-eq-1


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))
BY
{ ((ThinVar `x1' THEN (Subst' 1 ~ [[]] 0 THENA Computation))
   THEN Fold `member` 0
   THEN RepUR ``fdl-is-1`` 0
   THEN RepeatFor 2 (MemCD)
   THEN Try (Complete (Auto))
   THEN ((EqTypeHD (-1) THENA Auto) ORELSE (MemCD THEN EqTypeCD THEN Auto))) }

1
1. X : Type
2. x : Base
3. x ∈ X List List
4. x1 : x = [[]] ∈ pertype(λas,bs. ((as ∈ X List List) ∧ (bs ∈ X List List) ∧ dlattice-eq(X;as;bs)))
5. x ∈ X List List
6. [[]] ∈ X List List
7. dlattice-eq(X;x;[[]])
⊢ Ax ∈ ↑(∃a∈x.isaxiom(a))_b

2
.....antecedent..... 
1. X : Type
2. x : Base
3. x ∈ X List List
4. x1 : ↑(∃a∈x.isaxiom(a))_b@i
⊢ dlattice-eq(X;x;[[]])

---

Latex:

---

Latex:

1.  X  :  Type
2.  x  :  Base
3.  x1  :  Base
4.  x  =  x1
5.  x  \mmember{}  X  List  List
6.  x1  \mmember{}  X  List  List
7.  dlattice-eq(X;x;x1)
\mvdash{}  <\mlambda{}x.Ax,  \mlambda{}x.Ax>  =  <\mlambda{}x.Ax,  \mlambda{}x.Ax>


By

---

Latex:
((ThinVar  `x1'  THEN  (Subst'  1  \msim{}  [[]]  0  THENA  Computation))
  THEN  Fold  `member`  0
  THEN  RepUR  ``fdl-is-1``  0
  THEN  RepeatFor  2  (MemCD)
  THEN  Try  (Complete  (Auto))
  THEN  ((EqTypeHD  (-1)  THENA  Auto)  ORELSE  (MemCD  THEN  EqTypeCD  THEN  Auto)))

---

Home Index