proposition: Lemma exists_freq_hd A (x : A) g' (g : nat -> G A) (l : nat -> seq (nat * G A)) n : (exists s : nat, semProd (g s) x) -> exists s : nat, semProd (freq_ g' ((S n, g s) :: (l s))) x.
proof: Proof. intros Hin. inv Hin. eexists. eapply (@semFrequency A). simpl. eexists. split; eauto. now left. eassumption. Qed.
imports: String micromega.Lia List Tactics TacticsUtil Instances Classes DependentClasses Sets Producer Generators EnumProofs Checker Decidability CheckerProofs mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) Ltac2(Ltac2)