proposition: Lemma exists_freq_tl A (x : A) g' (g : nat -> G A) (l : nat -> seq (nat * G A)) n : (exists s : nat, match l s with | (S n, g1) :: gs => semProd (freq_ g' ((S n, g1) :: gs)) x | _ => False end) -> exists s : nat, semProd (freq_ g' ((S n, g s) :: (l s))) x.
proof: Proof. intros Hin. inv Hin. eexists. eapply (@semFrequency A). simpl. destruct (l x0) eqn:Heq. - exfalso; eauto. - destruct p. destruct n0; try (now (exfalso; eauto)). eapply (@semFrequency A) in H. rewrite Heq. simpl in H. inv H. destruct H0. eexists. split > [ | eassumption ]. now right; eauto. 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)