---

Step * of Lemma decidable__squash-list-match

∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
  ((∀a:A. ∀b:B.  Dec(R[a;b])) ⇒ (∀as:A List. ∀bs:B List.  Dec(↓list-match(as;bs;a,b.R[a;b]))))
BY
{ (InstLemma `decidable__squash-list-match-aux-ext` [] THEN RepeatFor 4 ((ParallelLast' THENA Auto))) }

1
1. [A] : Type
2. [B] : Type
3. [R] : A ⟶ B ⟶ ℙ
4. ∀a:A. ∀b:B.  Dec(R[a;b])
5. ∀bs:B List. ∀as:A List. ∀used:ℤ List.  Dec(↓list-match-aux(as;bs;used;a,b.R[a;b]))
⊢ ∀as:A List. ∀bs:B List.  Dec(↓list-match(as;bs;a,b.R[a;b]))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a:A.  \mforall{}b:B.    Dec(R[a;b]))  {}\mRightarrow{}  (\mforall{}as:A  List.  \mforall{}bs:B  List.    Dec(\mdownarrow{}list-match(as;bs;a,b.R[a;b]))))


By

---

Latex:
(InstLemma  `decidable\_\_squash-list-match-aux-ext`  []  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto)))

---

Home Index