---

Step * 1 of Lemma deq_subtype2

.....subterm..... T:t
1:n
1. T : Type
2. x : EqDecider(T)
⊢ x ∈ ∀x,y:T.  Dec(x = y ∈ T)
BY
{ (RepUR ``all decidable not implies`` 0
   THEN RepeatFor 2 ((FunExt THENA Auto))
   THEN RenameVar `a' (-2)
   THEN RenameVar `b' (-1)) }

1
1. T : Type
2. x : EqDecider(T)
3. a : T
4. b : T
⊢ x a b ∈ (a = b ∈ T) ∨ ((a = b ∈ T) ⟶ False)

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  T  :  Type
2.  x  :  EqDecider(T)
\mvdash{}  x  \mmember{}  \mforall{}x,y:T.    Dec(x  =  y)


By

---

Latex:
(RepUR  ``all  decidable  not  implies``  0
  THEN  RepeatFor  2  ((FunExt  THENA  Auto))
  THEN  RenameVar  `a'  (-2)
  THEN  RenameVar  `b'  (-1))

---

Home Index