proposition: Lemma in_dom_is_internal : forall (cfg : BDDconfig) (node : ad), in_dom _ node (fst cfg) = true -> is_internal_node cfg node.
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y. elim y; clear y; intros share counter. intros node H. elim (option_sum _ (MapGet _ (fst (bs, (share, counter))) node)). intros y. elim y. intro x. elim x. intro y0. intro y1. elim y1. intros y2 y3 y4. split with y0; split with y2; split with y3; assumption. intro y. unfold in_dom in H. rewrite y in H. discriminate H. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2