proposition: Lemma list_forall_exists_option_false : forall (A: Type) (f: A -> A -> option bool) (l1 l2 : list A), list_forall_option (fun t2: A => list_exists_option (fun t1: A => f t1 t2) l1) l2 = Some false -> (forall t2, In t2 l2 -> exists t1, In t1 l1 -> f t1 t2 = Some false) \/ (forall t2 : A, In t2 l2 -> exists t1 : A, In t1 l1 -> f t1 t2 = None -> False).
proof: Proof. intros. assert (H1:= @list_forall_option_is_sound A (fun t2 : A => list_exists_option (fun t1 : A => f t1 t2) l1) l2). rewrite H in H1. destruct H1. assert (exists a : A, In a l2 /\ exists t1, In t1 l1 -> f t1 a = Some false). destruct H0. destruct H0. exists x. split. trivial. assert (H4:= @list_exists_option_is_sound A (fun t1 : A => f t1 x) l1). rewrite H2 in H4. exists x. apply H4. assert (forall a : A, In a l2 -> exists t1, In t1 l1 -> f t1 a = None -> False). intros. assert (H2':= H1 a). assert ( list_exists_option (fun t1 : A => f t1 a) l1 = None -> False). apply H2'; trivial. assert (H6:= @list_exists_option_is_sound A (fun t1 : A => f t1 a) l1). case_eq (list_exists_option (fun t1 : A => f t1 a) l1). intros. destruct b. rewrite H5 in H6. destruct H6. destruct H6. exists x. intros. rewrite H9 in H7. discriminate. rewrite H5 in H6. exists a. intros. assert (H6':= H6 a). assert (f a a = Some false). apply H6'; trivial. rewrite H9 in H8. discriminate. intros. rewrite H5 in H6. destruct H6. destruct H6. exists x. intros. apply H4. trivial. right. assumption. 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)