proposition: Lemma branch_not_empty: forall A prefix brbit (m1 m2: ptrie A), m1 <> Empty -> m2 <> Empty -> branch prefix brbit m1 m2 = Branch prefix brbit m1 m2.
proof: Proof. intros; destruct m1; destruct m2; simpl; congruence. Qed.
imports: Lia Cdcl.Coqlib