proposition: Lemma exists_oneOf_hd A (x : A) g' (g : nat -> E A) (l : nat -> seq (E A)) : (exists s : nat, semProd (g s) x) -> 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. eexists. split; eauto. now left. 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)