pub fn binary_tree_path_ty() -> Expr
BinaryTreePath: a path (branch) through a binary tree up to length n. BinaryTreePath : Nat → Type