proposition: Lemma wf_branch': forall A p m m' (t1 t2: ptrie A), (forall n, (n >= m')%nat -> testbit p n = false) -> wf (Some (p, m, m', true)) t1 -> wf (Some (p, m, m', false)) t2 -> wf None (branch p m t1 t2).
proof: Proof. unfold branch; intros. inv H0; try constructor; auto. - inv H1; try econstructor; eauto. - inv H1; try econstructor; trivial; try congruence; try eassumption. + constructor; auto. + constructor; auto. + constructor; auto. + econstructor; trivial; try eapply H6; try eapply H7; try eassumption. - inv H1; try econstructor; trivial; try congruence; try eassumption. + econstructor; trivial; try eapply H7; try eapply H8; try eassumption. + econstructor; trivial. + econstructor; trivial; try eapply H7; try eapply H8; try eassumption. + econstructor; trivial; try eapply H6; try eapply H9; try eassumption. Qed.
imports: List Bool ZArith Lia