Heap allocated object in Idris2

Heap.idr

data Heap : Nat -> (Nat -> Type) -> Type where
  Lin : Heap Z a
  (:<) : Heap l a -> a l -> Heap (S l) a

data Tree : Nat -> Type where
  Leaf : String -> Tree n
  Branch : Fin n -> Fin n -> Tree n

u1 : Heap 4 Tree
u1 = [<
  Leaf "a",
  Leaf "b",
  Branch 0 1,
  Branch 2 2
]

data FVTree : {v : Type} -> (a : v -> Type) -> v -> Type where
  FVLeaf : 
    {v : Type} -> {a : v -> Type} -> {vi : v} ->
    String -> FVTree a vi
  FVBranch :
    {v : Type} -> {a : v -> Type} -> {vi : v} ->
    a vi -> a vi -> FVTree a vi

u2 : Heap 4 (FVTree Fin)
u2 = [<
  FVLeaf "a",
  FVLeaf "b",
  FVBranch 0 1,
  FVBranch 2 2
]