proposition: Theorem all_pbleaves_compute_pb : forall t, Permutation (map (fst (B:=_)) (compute_pbcode t)) (all_pbleaves t).
proof: Proof. cut (forall b l, map (fst (B:=_)) (map (fun v : A * list bool => let (a1, b1) := v in (a1, b :: b1)) l) = map (fst (B:=_)) l); [ intros HH | idtac ]. intros t; elim t; simpl in |- *; auto. intros p H; rewrite HH; auto. intros p H; rewrite HH; auto. intros p H p0 H0; rewrite map_app; apply Permutation_app; auto. repeat rewrite HH; auto. repeat rewrite HH; auto. intros b l; elim l; simpl in |- *; auto. intros a l0 H1; apply f_equal2 with (f := cons (A:=A)); auto. case a; simpl in |- *; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)