fact: Fixpoint try_all (s: list nat) (c: clause) (cs: clauses) (f: list nat -> clauses -> list (list nat)) {struct c}: list (list nat) := match c with nil => nil | (L p z) as k:: l1 => let s1 := update p z s in let cs1 := clauses_update k (anti_literals k) cs in merges (f s1 cs1) (try_all s l1 cs f) end.
imports: List UList Permutation Div OrderedList ListOp Lia