proposition: Lemma list_forall_option_is_complete_none : forall (A : Type) f l, (exists a, In a l /\ f a = None) -> @list_forall_option A f l = None.
proof: Proof. intros A f l; induction l as [ | a l]. simpl. intros. destruct H. destruct H. contradiction. intros. simpl in H. assert ((exists a0, a = a0 /\ f a0 = None) \/ (exists a0, In a0 l /\ f a0 = None)). destruct H. destruct H. destruct H. left. exists x. split; trivial. right. exists x. split;trivial. destruct H0. destruct H0. destruct H0. simpl. rewrite H0. rewrite H1. trivial. simpl. case_eq (f a). intros. destruct b. apply IHl. assumption. case_eq (list_forall_option f l). intros. assert (list_forall_option f l = None). apply IHl. assumption. rewrite H2 in H3. discriminate. intros. trivial. intros. trivial. 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)