---

Step * of Lemma mk_deq-subtype

∀[T,S:Type].  ∀[p:∀x,y:S.  Dec(x = y ∈ S)]. (mk_deq(p) ∈ EqDecider(T)) supposing strong-subtype(T;S)
BY
{ (Intros
   THEN Unhide
   THEN ((FLemma `strong-subtype-implies` [3] THENA Auto) THEN DoSubsume THEN Auto)
   THEN Unfold `deq` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,S:Type].    \mforall{}[p:\mforall{}x,y:S.    Dec(x  =  y)].  (mk\_deq(p)  \mmember{}  EqDecider(T))  supposing  strong-subtype(T;S)


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  ((FLemma  `strong-subtype-implies`  [3]  THENA  Auto)  THEN  DoSubsume  THEN  Auto)
  THEN  Unfold  `deq`  0
  THEN  Auto)

---

Home Index