proposition: Lemma bndngPatIndicesValid : forall {G:CFGV} (p: TermProd G), validBsl (length (tpRhsSym p)) (bndngPatIndices p).
proof: Proof. intros. unfolds_base. unfold bndngPatIndices. introv Hin. apply in_map_iff in Hin. exrepnd. subst. apply bsNthValid. Qed.
imports: GVariables