Lvc.Infra.Indexwise

Require Import Arith Coq.Lists.List Setoid Coq.Lists.SetoidList Omega Containers.OrderedTypeEx.
Require Export Infra.Option EqDec AutoIndTac Get.

Set Implicit Arguments.

Definition indexwise_R {A} {B} (R:A→B→Prop) LA LB :=
∀ n a b, get LA n a → get LB n b → R a b.

Definition indexwise_R_dec {A} {B} {R:A→B→Prop} (Rdec:(∀ a b, Computable (R a b))) LA LB
      : Computable (indexwise_R R LA LB) .
Defined.

Definition indexwise_R_dec´ {A} {B} {R:A→B→Prop} LA LB (Rdec:(∀ n a b, get LA n a → get LB n b → Computable (R a b)))
      : Computable (indexwise_R R LA LB).
Defined.