proposition: Lemma exists_oneOf_tl A (x : A) g' (g : nat -> E A) (l : nat -> seq (E A)) : (exists s : nat, match l s with | nil => False | g1 :: gs => semProd (oneOf_ g' (g1 :: gs)) x end) -> exists s : nat, semProd (oneOf_ g' ((g s) :: (l s))) x.
proof: Proof. intros Hin. inv Hin. eexists. eapply semOneof. now eauto with typeclass_instances. destruct (l x0) eqn:Heq. - exfalso; eauto. - eapply semOneof in H > [ | now eauto with typeclass_instances ]. rewrite Heq. inv H. destruct H0. eexists. split > [ | eassumption ]. now right; eauto. Qed.
imports: String micromega.Lia List Tactics TacticsUtil Instances Classes DependentClasses Sets Producer Enumerators Checker Decidability CheckerProofs Ltac2(Ltac2) mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq)