proposition: Lemma list_forall_exists_option_true : 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 true -> (forall t2, In t2 l2 -> exists t1, In t1 l1 /\ f t1 t2 = Some true).
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. assert (forall a : A, In a l2 -> exists t1, In t1 l1 /\ f t1 a = Some true). intros. assert (H1':= H1 a). assert ( list_exists_option (fun t1 : A => f t1 a) l1 = Some true). apply H1'; trivial. assert (H5:= @list_exists_option_is_sound A (fun t1 : A => f t1 a) l1). rewrite H3 in H5. destruct H5. destruct H4. exists x. intros. split. assumption. assumption. assert (H2':= H2 t2). assert ( exists t1 : A, In t1 l1 /\ f t1 t2 = Some true). apply H2'; trivial. destruct H3. exists x. intros. 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)