---

Step * 1 1 of Lemma deq_subtype2


1. T : Type
2. x : EqDecider(T)
3. a : T
4. b : T
⊢ x a b ∈ (a = b ∈ T) ∨ ((a = b ∈ T) ⟶ False)
BY
{ ((Unfold `deq` 2 THEN D 2) THEN (InstHyp [⌜a⌝;⌜b⌝] 3⋅ THENA Auto)) }

1
1. T : Type
2. x : T ⟶ T ⟶ 𝔹
3. ∀x@0,y:T.  (x@0 = y ∈ T ⇐⇒ ↑(x x@0 y))
4. a : T
5. b : T
6. a = b ∈ T ⇐⇒ ↑(x a b)
⊢ x a b ∈ (a = b ∈ T) ∨ ((a = b ∈ T) ⟶ False)

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  EqDecider(T)
3.  a  :  T
4.  b  :  T
\mvdash{}  x  a  b  \mmember{}  (a  =  b)  \mvee{}  ((a  =  b)  {}\mrightarrow{}  False)


By

---

Latex:
((Unfold  `deq`  2  THEN  D  2)  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  3\mcdot{}  THENA  Auto))

---

Home Index