proposition: Theorem try_all_olist: forall s c cs f, (forall s cs1, olist _ (lexico _ test) (f s cs1) ) -> olist _ (lexico _ test) (try_all s c cs f).
proof: Proof. intros s c cs f H; elim c; simpl; auto. apply olist_nil. intros (p, z) c1 Rec; unfold merges; apply merge_olist; auto. intros; apply lexico_trans; auto. exact test_trans. intros; apply test_anti_sym; auto. exact test_compat_l. intros; apply lexico_anti_sym; auto. intros; apply test_anti_sym; auto. intros; apply lexico_exact with (weight := test); auto. exact test_exact. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia