---

Step * of Lemma decidable__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
{ Auto }

1
.....decidable?..... 
1. [A] : Type
2. [B] : Type
3. [R] : A ⟶ B ⟶ ℙ
4. ∀a:A. ∀b:B.  Dec(R[a;b])
5. as : A List
6. 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(list-match(as;bs;a,b.R[a;b]))))


By

---

Latex:
Auto

---

Home Index