proposition: Theorem decode_correct : forall c : code, unique_prefix c -> not_null c -> forall (m1 m2 : list bool) (a : A), find_val m1 c = Some a -> decode c (m1 ++ m2) = a :: decode c m2.
proof: Proof. intros c H H0 m1 m2 a H1; unfold decode in |- *; apply decode_aux_correct; auto. Qed.
imports: Coq(Sorting.Permutation)