fact: Definition content := (fix loop (acc : env N) s := match s with | Leaf n => set_pos_trec 0%num N.succ [::] acc n | Op s s' => loop (loop acc s') s end) Empty.
imports: HB(structures) BinPos BinNat mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq bigop)