proposition: Lemma backtrack_SizeMonotonicOpt (A : Type) (l : list (nat * G (option A))) : l \subset (fun x => SizeMonotonicOpt x.2) -> SizeMonotonicOpt (backtrack l).
proof: Proof. intros Hin. intros s1 s2 Hleq. rewrite !backtrack_correct_size_opt. intros x Hin'. destruct Hin' as [e [Hl Hs]]. eexists. split; eauto. eapply Hin; inv Hl; eauto. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)