fact: Fixpoint get (T:Type) (a:pos) (u:table T) {struct a} : T := match a with one => match u with stop x => x | node x v w => x end | xL b => match u with stop x => x | node x v w => (get b v) end | xR b => match u with stop x => x | node x v w => (get b w) end end.