---

Step * 1 of Lemma streamless-dec-equal

.....decidable?..... 
1. [T] : Type
2. streamless(T)
3. x : T
4. y : T
⊢ Dec(x = y ∈ T)
BY
{ xxx(Unfold `streamless` 2
      THEN (Skolemize 2 `F'  THENA Auto)
      THEN (InstHyp [⌜λn.x⌝] (-1)⋅ THENA Auto)
      THEN Reduce (-1)
      THEN ExRepD)xxx }

1
1. [T] : Type
2. ∀f:ℕ ⟶ T. ∃i,j:ℕ. ((¬(i = j ∈ ℕ)) ∧ ((f i) = (f j) ∈ T))
3. x : T
4. y : T
5. F : f:(ℕ ⟶ T) ⟶ ℕ
6. ∀f:ℕ ⟶ T. ∃j:ℕ. ((¬((F f) = j ∈ ℕ)) ∧ ((f (F f)) = (f j) ∈ T))
7. j : ℕ
8. ¬((F (λn.x)) = j ∈ ℕ)
9. x = x ∈ T
⊢ Dec(x = y ∈ T)

---

Latex:

---

Latex:
.....decidable?..... 
1.  [T]  :  Type
2.  streamless(T)
3.  x  :  T
4.  y  :  T
\mvdash{}  Dec(x  =  y)


By

---

Latex:
xxx(Unfold  `streamless`  2
        THEN  (Skolemize  2  `F'    THENA  Auto)
        THEN  (InstHyp  [\mkleeneopen{}\mlambda{}n.x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
        THEN  Reduce  (-1)
        THEN  ExRepD)xxx

---

Home Index