proposition: Theorem correct_encoding : forall c : code, unique_prefix c -> not_null c -> forall m : list A, in_alphabet m c -> decode c (encode c m) = m.
proof: Proof. intros c H1 H2 m; elim m; simpl in |- *; auto. intros H3; unfold decode in |- *; simpl in |- *. rewrite not_null_find_val; auto. intros a l H H0; rewrite decode_correct with (a := a); auto. apply f_equal2 with (f := cons (A:=A)); auto. apply H; apply in_alphabet_inv with (1 := H0); auto. case (H0 a); simpl in |- *; auto. intros l1 Hl1. apply find_val_correct2; auto. case (H0 a); simpl in |- *; auto. intros x1; case x1. intros H3; case (H2 a); auto. intros b l0 H3; cut (find_code a c = b :: l0). intros H4; rewrite H4; apply find_code_correct1; auto. apply find_code_correct2 with (2 := H3); auto. case H1; auto. Qed.
imports: Coq(Sorting.Permutation)