---

Step * of Lemma product-deq_wf

∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)].  (product-deq(A;B;a;b) ∈ EqDecider(A × B))
BY
{ TACTIC:(Auto
          THEN Unfold `deq` 0
          THEN RepeatFor 2 (ProveWfLemma)
          THEN MemTypeCD
          THEN (RepeatFor 2 (((D 0 THENA Auto) THEN D -1 THEN Reduce 0)) ORELSE Auto)
          THEN RW assert_pushdownC 0
          THEN Auto
          THEN EqHD (-1)
          THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[a:EqDecider(A)].  \mforall{}[b:EqDecider(B)].    (product-deq(A;B;a;b)  \mmember{}  EqDecider(A  \mtimes{}  B))


By

---

Latex:
TACTIC:(Auto
                THEN  Unfold  `deq`  0
                THEN  RepeatFor  2  (ProveWfLemma)
                THEN  MemTypeCD
                THEN  (RepeatFor  2  (((D  0  THENA  Auto)  THEN  D  -1  THEN  Reduce  0))  ORELSE  Auto)
                THEN  RW  assert\_pushdownC  0
                THEN  Auto
                THEN  EqHD  (-1)
                THEN  Auto)

---

Home Index