proposition: Lemma lBoundVarsLenSameifNth : forall {G : CFGV} ( vc : VarSym G) {la : list (bool # GSym G)} (ma mb: Mixture la), (forall (nn : nat), length (getBVarsNth vc ma nn) = length (getBVarsNth vc mb nn)) -> forall (lln : list (list nat)), map (@length _) (lBoundVars vc lln ma) = map (@length _) (lBoundVars vc lln mb).
proof: Proof. intros. unfold lBoundVars. rewrite map_map. rewrite map_map. unfold compose. apply eq_maps. intros n Hin. clear Hin. induction n; allsimpl; cpx. rewrite length_app. rewrite length_app. f_equal; cpx. Qed.
imports: CFGV Omega