---

Step * of Lemma list-deq_wf

∀[A:Type]. ∀[eq:EqDecider(A)].  (list-deq(eq) ∈ EqDecider(A List))
BY
{ (Auto
   THEN MemTypeCD
   THEN Try (Complete (Auto))
   THEN RepeatFor 2 (InductionOnList)
   THEN Auto
   THEN Try (Complete ((All (RepUR ``list-deq``) THEN Auto)⋅))
   THEN (Assert list-deq(eq) [u / v] [u1 / v1] ~ (eq u u1) ∧b (list-deq(eq) v v1) BY
               (RepUR ``list-deq`` 0 THEN Auto))
   THEN RWW "-1" 0
   THEN RWW "-1" (-2)
   THEN Thin (-1)
   THEN (InstHyp [⌜v1⌝] (-6)⋅ THENA Auto)
   THEN (RepeatFor 2 (MoveToConcl (-1))
         THEN GenConcl ⌜list-deq(eq) v v1 = b⌝⋅
         THEN RW assert_pushdownC 0
         THEN Auto
         THEN EqCD
         THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].    (list-deq(eq)  \mmember{}  EqDecider(A  List))


By

---

Latex:
(Auto
  THEN  MemTypeCD
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  2  (InductionOnList)
  THEN  Auto
  THEN  Try  (Complete  ((All  (RepUR  ``list-deq``)  THEN  Auto)\mcdot{}))
  THEN  (Assert  list-deq(eq)  [u  /  v]  [u1  /  v1]  \msim{}  (eq  u  u1)  \mwedge{}\msubb{}  (list-deq(eq)  v  v1)  BY
                          (RepUR  ``list-deq``  0  THEN  Auto))
  THEN  RWW  "-1"  0
  THEN  RWW  "-1"  (-2)
  THEN  Thin  (-1)
  THEN  (InstHyp  [\mkleeneopen{}v1\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)
  THEN  (RepeatFor  2  (MoveToConcl  (-1))
              THEN  GenConcl  \mkleeneopen{}list-deq(eq)  v  v1  =  b\mkleeneclose{}\mcdot{}
              THEN  RW  assert\_pushdownC  0
              THEN  Auto
              THEN  EqCD
              THEN  Auto)\mcdot{})

---

Home Index