proposition: Lemma semProdOpt_failEnum A : semProdOpt failEnum <--> (@set0 A).
proof: Proof. intro x; split; intros H1. inv H1. inv H. now inv H1. now inv H1. 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)