proposition: Lemma bndngPatIndicesValid2 : forall {G:CFGV} (p: TermProd G), validBsl (length (snd (tpLhsRhs G p))) (bndngPatIndices p).
proof: Proof. intros. pose proof (bndngPatIndicesValid p) as X. unfold tpRhsSym in X. autorewrite with fast in X. trivial. Qed.
imports: GVariables