proposition: Lemma ValidIndicesDecidable: forall {A B : Type} (bindingInfo : list (nat * nat)) (rhsSyms : list (A + B)), decidable (ValidIndices bindingInfo rhsSyms).
proof: Proof. intros. unfold ValidIndices. apply decidable_prod;[|apply decidable_prod]. - induction bindingInfo as [| (n,m) bindingInfo Hind]; [left; dands |]; cpx. dorn Hind;[| right]; cpx. remember (liftNth isInl rhsSyms n) as bl. destruct (lt_dec m (length rhsSyms)); destruct (lt_dec n (length rhsSyms)); destruct bl; try rewrite <- Heqbl; try(left; introv Hin; repeat(in_reasoning); cpx; fail); [| | | | | | ]; right; introv Hin; specialize (Hin _ _ (inl eq_refl)); try rewrite <- Heqbl in Hin; dands; cpx. - remember ((map (fst (B:=nat)) bindingInfo)) as bif. clear dependent bindingInfo. revert bif. unfold liftNth; induction rhsSyms as [| rs rhsSyms Hind]; [left; intro n; destruct n; simpl; cpx |]. intro bifCons. remember (flat_map (fun n=> match n with |0 => [] | S m => [m] end) bifCons) as bif. specialize (Hind bif). dorn Hind; [| right]; cpx. + destruct rs as [sa| sb];[|left; destruct n; allsimpl; cpx]. * destruct (in_deq _ deq_nat 0 bifCons); cpx; [left; destruct n | right]; simpl; subst bif; cpx;[]. introv Heq. apply Hind in Heq. apply lin_flat_map in Heq. exrepnd. destruct x; cpx. inverts Heq0; cpx; fail. * introv Heq. subst bif. specialize (Hind ( n)). apply Hind in Heq. clear Hind. apply lin_flat_map in Heq. exrepnd. destruct x; cpx. inverts Heq0; cpx. + introv Hc. apply Hind. clear Hind. introv Heq. subst bif. apply lin_flat_map. specialize (Hc (S n)). simpl in Hc. apply Hc in Heq. exists (S n). dands; cpx. - apply no_repeat_dec. apply deq_prod; exact deq_nat. Defined.
imports: GVariables