fact: Fixpoint Tremove (p:positive) (T:Tree) {struct p}: Tree := match T with | Tempty => Tempty | Branch0 T1 T2 => match p with | xI pp => mkBranch0 T1 (Tremove pp T2) | xO pp => mkBranch0 (Tremove pp T1) T2 | xH => T end | Branch1 b T1 T2 => match p with | xI pp => Branch1 b T1 (Tremove pp T2) | xO pp => Branch1 b (Tremove pp T1) T2 | xH => mkBranch0 T1 T2 end end.
imports: List BinPos