proposition: Lemma list_exists_option_decomposed: forall (A: Type) (f : A -> option bool) (l: list A) (t: A), f t = Some false -> (list_exists_option f (t :: l) = Some true <-> list_exists_option f l = Some true).
proof: Proof. intros. simpl. rewrite H. reflexivity. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)