Patent parent function is a rooted tree (Sym2)

import Definitions.Def_HypercubeLineVIST_sym2parent
import Definitions.Def_HypercubeLineVIST_patentParent

theorem HypercubeLineVISTPatent_isTree (n : Nat) (hn : 3 < n)
    (r : Sym2 (Fin n → Bool)) (a b : Fin n → Bool) (d0 : Fin n)
    (k : HypercubeLineVISTSym2.TreeIdx n) (v : Sym2 (Fin n → Bool)) :
    HypercubeLineVISTSym2.patentParentSym2 n (by omega) r a b d0 k r = r := by
  sorry