proposition: Lemma keys_norepet': forall (A: Type) (m: ptrie A) opt, wf opt m -> list_norepet (keys' m).
proof: Proof. induction m; intros. - constructor. - constructor; auto. constructor. - unfold keys'. rewrite elements_branch'. rewrite map_app. apply list_norepet_append. + inv H; eapply IHm1; eauto. + inv H; eapply IHm2; eauto. + red; intros. eapply in_map_iff in H0; eapply in_map_iff in H1. destruct H0 as [x1 [HA HB]]. destruct H1 as [x2 [HC HD]]. destruct x1; destruct x2; subst. simpl. inv H. * eapply in_elements' in HB; eauto. eapply in_elements' in HD; eauto. destruct HB; auto. destruct HD; auto. case_eq (Key.zerobit e brbit); intros; case_eq (Key.zerobit e0 brbit); intros. { generalize (get_not_same_lr H6 H2). congruence. } { red; intros; congruence. } { generalize (get_not_same_lr H3 H1). congruence. } { generalize (get_not_same_lr H3 H1). congruence. } * eapply in_elements' in HB; eauto. eapply in_elements' in HD; eauto. destruct HB; auto. destruct HD; auto. case_eq (Key.zerobit e brbit); intros; case_eq (Key.zerobit e0 brbit); intros. { generalize (get_not_same_lr H6 H2). congruence. } { red; intros; congruence. } { generalize (get_not_same_lr H3 H1). congruence. } { generalize (get_not_same_lr H3 H1). congruence. } Qed.
imports: Lia Cdcl.Coqlib