proposition: Theorem ordered_cover_subst_pred : forall (t1 : btree A) (l1 l2 : list (btree A)), ordered_cover l1 t1 -> length l1 = length l2 -> exists t2 : btree A, subst_pred l1 l2 t1 t2.
proof: Proof. intros t1 l1 l2 H; generalize l2; elim H; clear t1 l1 l2 H. intros t l l2; case l2. simpl in |- *; intros; discriminate. intros b l0; case l0; simpl in |- *; auto. intros H; exists b; auto. intros; discriminate. intros t1 t2 l1 l2 l3 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. 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 HH2. exists (node t4 t5); auto. rewrite <- (firstn_skipn (length l1) l0); auto. Qed.
imports: Huffman(HeightPred)