fact: Fixpoint DGTree_ind2 (t : DGTree) : P t := match t as x return P x with DGNode a l => H a l ((fix l_ind (l' : list DGTree) : Q l' := match l' as x return Q x with | nil => H0 | cons t1 tl => H1 t1 (DGTree_ind2 t1) tl (l_ind tl) end) l) 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)