proposition: Lemma lBoundVarsSameifNth : forall {G : CFGV} ( vc : VarSym G) {la : list (bool # GSym G)} (ma mb: Mixture la), (forall (nn : nat), getBVarsNth vc ma nn = getBVarsNth vc mb nn) -> forall (lln : list (list nat)), lBoundVars vc lln ma = lBoundVars vc lln mb.
proof: Proof. intros. unfold lBoundVars. apply eq_maps. intros n Hin. apply eq_flat_maps. intros nn Hinn. cpx. Qed.
imports: CFGV Omega