---

Step * of Lemma decidable__equal_set

∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀[P:T ⟶ Type]. ∀x,y:{x:T| P[x]} .  Dec(x = y ∈ {x:T| P[x]} )))
BY
{ (Auto THEN ((InstHyp [⌜x⌝; ⌜y⌝] 2)⋅ THENA Auto)) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. [P] : T ⟶ Type
4. x : {x:T| P[x]} @i
5. y : {x:T| P[x]} @i
6. Dec(x = y ∈ T)
⊢ Dec(x = y ∈ {x:T| P[x]} )

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}[P:T  {}\mrightarrow{}  Type].  \mforall{}x,y:\{x:T|  P[x]\}  .    Dec(x  =  y)))


By

---

Latex:
(Auto  THEN  ((InstHyp  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{}]  2)\mcdot{}  THENA  Auto))

---

Home Index