The (positions of elements in a binary tree) and (the positions in its inorder traversal) are isomorphic.

Inord.idr

import Data.List
%default total

data Tree : Type -> Type where
  Tip  : Tree a
  Node : (x : a) -> (l : Tree a) -> (r : Tree a) -> Tree a
%name Tree t, u

data InTree : a -> Tree a -> Type where
  Here  : InTree x (Node x l r)
  Left  : InTree x l -> InTree x (Node y l r)
  Right : InTree x r -> InTree x (Node y l r)

inorder : Tree a -> List a
inorder Tip          = []
inorder (Node x l r) = inorder l ++ [x] ++ inorder r

infixr 5 ++^ , ^++
(^++) : (xs : List a) -> Elem x ys -> Elem x (xs ++ ys)
[]        ^++ e = e
(x :: xs) ^++ e = There (xs ^++ e)

(++^) : Elem x xs -> (ys : List a) -> Elem x (xs ++ ys)
Here      ++^ ys = Here
(There x) ++^ ys = There (x ++^ ys)

data SplitRes : (x : a) -> (xs, ys : List a) -> (e : Elem x (xs ++ ys)) -> Type where
  SLeft  : (e' : Elem x xs) -> e' ++^ ys = e -> SplitRes x xs ys e
  SRight : (e' : Elem x ys) -> xs ^++ e' = e -> SplitRes x xs ys e
  
listSplit : (xs, ys : List a) -> (e : Elem x (xs ++ ys)) -> SplitRes x xs ys e
listSplit [] (x :: xs) Here = SRight Here Refl
listSplit (x :: xs) ys Here = SLeft Here Refl
listSplit [] (y :: xs) (There e) with (listSplit [] xs e)
  | (SLeft Here prf) impossible
  | (SRight e' prf) = SRight (There e) Refl
listSplit (y :: xs) ys (There e) with (listSplit xs ys e)
  listSplit (_ :: _) _ (There _) | SLeft  e' Refl = SLeft (There e') Refl
  listSplit (_ :: _) _ (There _) | SRight e' Refl = SRight e' Refl

unsplitRight : 
  (xs : List a) -> (e : Elem x ys) -> listSplit xs ys (xs ^++ e) = SRight e Refl
unsplitRight [] Here      = Refl
unsplitRight [] (There e) = rewrite unsplitRight [] e in Refl
unsplitRight (x :: xs) e  = rewrite unsplitRight xs e in Refl      

unsplitLeft : 
  (e : Elem x xs) -> (ys : List a) -> listSplit xs ys (e ++^ ys) = SLeft e Refl
unsplitLeft Here      ys = Refl
unsplitLeft (There e) ys = rewrite unsplitLeft e ys in Refl

ElemToInTree : (t : Tree a) -> Elem x (inorder t) -> InTree x t
ElemToInTree Tip Here impossible
ElemToInTree (Node x l r) e with (listSplit (inorder l) (x :: inorder r) e)
  | SLeft e' _          = Left (ElemToInTree l e')
  | SRight Here _       = Here
  | SRight (There e') _ = Right (ElemToInTree r e')
  
InTreeToElem : InTree x t -> Elem x (inorder t)
InTreeToElem (Here {l})         = inorder l ^++ Here
InTreeToElem (Left {y}{l}{r} e) = InTreeToElem e ++^ (y :: inorder r)
InTreeToElem (Right {y}{l} e)   = inorder l ^++ [y] ^++ InTreeToElem e

inorderToFro : (e : InTree x t) -> ElemToInTree t (InTreeToElem e) = e
inorderToFro {x = x} (Here {l}{r}) = 
  rewrite unsplitRight {ys = x :: inorder r}(inorder l) Here in Refl
inorderToFro (Left {y}{l}{r} e) = 
  rewrite unsplitLeft (InTreeToElem e) (y :: inorder r) in 
  rewrite inorderToFro e in Refl
inorderToFro (Right {y}{l}{r} e) =
  rewrite unsplitRight (inorder l) (There {xs = inorder r}{y = y} (InTreeToElem e)) in
  rewrite inorderToFro e in Refl
  
inorderFroTo : (t : Tree a) -> (e : Elem x (inorder t)) -> InTreeToElem (ElemToInTree t e) = e
inorderFroTo Tip Here impossible
inorderFroTo (Node x l r) e with (listSplit (inorder l) (x :: inorder r) e)
  | SLeft  el         prf = rewrite inorderFroTo l el in prf
  | SRight Here       prf = prf
  | SRight (There er) prf = rewrite inorderFroTo r er in prf