proposition: Lemma set'_not_empty: forall A k x (pt: ptrie A), set' k x pt <> Empty.
proof: Proof. intros; induction pt; simpl; try congruence. - destruct (eqb k k0)eqn:EQ; try congruence. unfold join; simpl. destruct (zerobit k (branching_bit k k0)); discriminate. - destruct (match_prefix k prefix brbit). + destruct (zerobit k brbit); discriminate. + unfold join; simpl. destruct (zerobit k (branching_bit k prefix)); discriminate. Qed.
imports: List Bool ZArith Lia