proposition: Lemma xcombine'_not_empty: forall A c (t1 t2: ptrie A), t1 <> Empty \/ t2 <> Empty -> xcombine' c t1 t2 <> Empty.
proof: Proof. induction t1; intros. - destruct H; try congruence. destruct t2; simpl; congruence. - destruct H; destruct t2; unfold xcombine'; try congruence; eapply insert'_not_empty. - destruct H; destruct t2; unfold xcombine'; try congruence. + eapply insert'_not_empty. + unfold join; destruct (eqb prefix prefix0 && eqb brbit brbit0); destruct (ltb brbit brbit0 && match_prefix prefix0 prefix brbit); destruct (zerobit prefix0 brbit); destruct (ltb brbit0 brbit && match_prefix prefix prefix0 brbit0); destruct (zerobit prefix brbit0); destruct (zerobit prefix (branching_bit prefix prefix0)); try discriminate . + eapply insert'_not_empty. + unfold join; destruct (eqb prefix prefix0 && eqb brbit brbit0); destruct (ltb brbit brbit0 && match_prefix prefix0 prefix brbit); destruct (zerobit prefix0 brbit); destruct (ltb brbit0 brbit && match_prefix prefix prefix0 brbit0); destruct (zerobit prefix brbit0); destruct (zerobit prefix (branching_bit prefix prefix0)); try discriminate . Qed.
imports: List Bool ZArith Lia