fact: Fixpoint compute_code (a : btree) : list (A * list bool) := match a with | leaf b => (b, []) :: [] | node l1 l2 => map (fun v : A * list bool => match v with | (a1, b1) => (a1, false :: b1) end) (compute_code l1) ++ map (fun v : A * list bool => match v with | (a1, b1) => (a1, true :: b1) end) (compute_code l2) end.
imports: Coq(ArithRing ListDec)