fact: Fixpoint tree_P3 {a} (a_C : C a) (t : tree a) : bool := let tree_C := Build_C _ (tree_P3 a_C) in match t with Node _ x ts => orb (P x) (P (C:=list_C tree_C) ts) end.
imports: Equations(Equations) Coq.Lists.List