proposition: Lemma P3_test2 (t : tree a) : tree_P3 t = true -> exists x, In x (elements t) /\ P x = true.
proof: Proof. revert a a_C t. refine (proj1 (my_P3_elim (fun a a_C t b => b = true -> exists x : a, In x (elements t) /\ P x = true) (fun a aC (t : list (tree a)) b => b = true -> exists x : a, In x (list_elements t) /\ P x = true) _ _ _)); clear; intros. rename H0 into Hal. - rewrite orb_true_iff in Hal. destruct Hal as [Hal|Hal]. + exists a0. simp elements. intuition auto with datatypes. + specialize (H Hal). simp elements. destruct H as (ex & exl & Pexl). simp elements in *. exists ex. simpl. intuition auto. - discriminate. - simpl in H1. rewrite orb_true_iff in H1. destruct H1. specialize (H H1). firstorder. exists x. simpl. rewrite in_app_iff. firstorder. specialize (H0 H1). simpl. destruct H0. exists x. rewrite in_app_iff; firstorder. Qed.
imports: Equations(Equations) Coq.Lists.List Bool