proposition: Lemma bsNthValid : forall {G:CFGV} (p: TermProd G) (k:nat), ValidNthSrc (length (tpRhsSym p)) (bindingSourcesNth p k).
proof: Proof. intros. unfold ValidNthSrc. unfold bindingSourcesNth, bindingInfo, tpRhsSym. autorewrite with fast. pose proof (bindingInfoCorrect G p) as XX. destruct (tpLhsRhs G p) as [lhs ls]. destruct G; allsimpl; cpx. allsimpl. remember ((bindingInfo0 p)) as bi. clear Heqbi. allsimpl. clear bindingInfoCorrect0. repnud XX. clear XX1. induction bi; dands; allsimpl; cpx; allrw no_repeats_cons; exrepnd; apply IHbi in XX1; exrepnd; cpx; remember (beq_nat k a) as bn; destruct bn; cpx; allrw no_repeats_cons; allsimpl; dands; cpx. - introv Hin. rw lin_flat_map in Hin. exrepnd. remember (beq_nat k x) as bkx; destruct bkx; allsimpl; cpx. dorn Hin0; subst; cpx. allapply beq_nat_eq. subst. subst. cpx. - pose proof (XX0 _ _ (inl eq_refl)). repnd; cpx. Qed.
imports: GVariables