fact: Fixpoint L_subtree {A:Type} (p:path) (t:LTree A) {struct p} : option (LTree A) := match p with | nil => Some t | d0 :: p' => match t with | LLeaf => None | LBin a t1 t2 => L_subtree p' t1 end | d1 :: p' => match t with | LLeaf => None | LBin a t1 t2 => L_subtree p' t2 end end.
imports: List