proposition: Lemma P3_test (t : tree a) : tree_P3 t = true -> exists x, In x (elements t) /\ P x = true.
proof: Proof. revert t. refine (tree_elim (P0:=fun t : list (tree a) => list_P3 t = true -> exists x : a, In x (list_elements t) /\ P x = true) _ _ _); clear; intros. simp tree_P3 in H0. rename H0 into Hal. - rewrite orb_true_iff in Hal. destruct Hal as [Hal|Hal]. + exists a0. simp elements. intuition auto with datatypes. + simp tree_P3 in H. specialize (H Hal). simp elements. destruct H as (ex & exl & Pexl). simp elements in *. exists ex. simpl. intuition auto. - simpl in H. 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