proposition: Theorem subst_pred_ordered_cover_r : forall (t1 t2 : btree A) (l1 l2 : list (btree A)), subst_pred l1 l2 t1 t2 -> ordered_cover l2 t2.
proof: Proof. intros t1 t2 l1 l2 H; elim H; auto. Qed.
imports: Huffman(HeightPred)