proposition: Theorem subst_pred_length : forall (t1 t2 : btree A) (l1 l2 : list (btree A)), subst_pred l1 l2 t1 t2 -> length l1 = length l2.
proof: Proof. intros t1 t2 l1 l2 H; elim H; auto. intros t0 t3 t4 t5 l0 l3 l4 l5 l6 l7 H0 H1 H2 H3; repeat rewrite app_length; auto. Qed.
imports: Huffman(HeightPred)