fact: Fixpoint ltree_ind2 (t : ltree A) : P t := match t as x return P x with lnode _ a l => H a l ((fix l_ind (l' : list (ltree A)) : Q l' := match l' as x return Q x with nil => H0 | cons t1 tl => H1 t1 (ltree_ind2 t1) tl (l_ind tl) end) l) end.
imports: List