proposition: Lemma initBDDsharing_map_OK : BDDsharing_OK initBDDstate initBDDsharing_map.
proof: Proof. unfold BDDsharing_OK, initBDDstate, initBDDsharing_map in |- *. split. intros H. compute in H. discriminate H. intros H. compute in H. discriminate H. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat