fact: Fixpoint InDGTree (dg : Location) (tree : DGTree) : bool := match tree with | DGNode f kids => if LocDec.eq_dec dg f then true else fold_right (fun tree' => (orb (InDGTree dg tree'))) false kids end.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)