proposition: Lemma semProdOpt_return_None {A} : semProdOpt (returnEnum None) <--> (@set0 A).
proof: Proof. intro x; split; intro H; inv H. inv H0. inv H1. congruence. inv H0. 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)