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