---

Step * of Lemma deq_functionality_wrt_ext-eq

∀[A,B:Type].  EqDecider(A) ≡ EqDecider(B) supposing A ≡ B
BY
{ (Auto
   THEN ParallelLast
   THEN Auto
   THEN D 0
   THEN Auto
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN FHyp (-4) [-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    EqDecider(A)  \mequiv{}  EqDecider(B)  supposing  A  \mequiv{}  B


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  FHyp  (-4)  [-1]
  THEN  Auto)

---

Home Index