proposition: Theorem unique_prefix1 : forall (c : code) (a1 a2 : A) (lb1 lb2 : list bool), unique_prefix c -> In (a1, lb1) c -> In (a2, lb2) c -> is_prefix lb1 lb2 -> a1 = a2.
proof: Proof. intros c a1 a2 lb1 lb2 (H1, H2); apply (H1 a1 a2 lb1 lb2); auto. Qed.
imports: Coq(Sorting.Permutation)