proposition: Theorem height_pred_subst_pred : forall (n : nat) (ln : list nat) (t1 : btree A) (l1 l2 : list (btree A)), height_pred n ln l1 t1 -> length l1 = length l2 -> exists t2 : btree A, height_pred n ln l2 t2 /\ subst_pred l1 l2 t1 t2.
proof: Proof. intros n ln t1 l1 l2 H; generalize l2; elim H; clear H n ln t1 l1 l2; auto. intros n t l2; case l2. simpl in |- *; intros; discriminate. intros b l0; case l0; intros; try discriminate; exists b; auto. intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 l0 H3. case (H0 (firstn (length l1) l0)); auto. rewrite firstn_le_length_eq; auto; (rewrite <- H3; rewrite app_length; auto with arith). intros t4 (HH1, HH2). case (H2 (skipn (length l1) l0)); auto. rewrite skipn_length; auto; (rewrite <- H3; rewrite app_length; rewrite <- Nat.add_comm; rewrite Nat.add_sub; auto with arith). intros t5 (HH3, HH4). exists (node t4 t5); rewrite <- (firstn_skipn (length l1) l0); auto. Qed.
imports: Huffman(HeightPred)