fact: Fixpoint find_just_one_aux (n: clauses) (s: list nat) (cs: clauses) : jRes := match cs with nil => jOne s | (_, nil) :: _ => jNone | (_, p) :: cs1 => match n with nil => jNone | _ :: n1 => try_just_one s p cs1 (find_just_one_aux n1) end end.
imports: List UList Permutation Div OrderedList ListOp Lia