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: ZArith List Arith Zwf Relations Inverse_Image