proposition: Lemma semProd_mon {A} (g : nat -> G A) {_ : SizedMonotonic g} : forall s1 s2, (s1 <= s2)%coq_nat -> semProd (g s1) \subset semProd (g s2).
proof: Proof. intros s1 s2 Hleq. intros x Hin. inv Hin. inv H0. eexists x0. split; eauto. eapply H > [ | eassumption ]. destruct (leqP s1 s2); 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)