proposition: Lemma BDDvar_make_node_OK : forall (cfg : BDDconfig) (x : BDDvar), BDDconfig_OK cfg -> config_node_OK (fst (BDDvar_make cfg x)) (snd (BDDvar_make cfg x)).
proof: Proof. intros. refine (proj2 (proj2 (proj2 (proj2 (BDDmake_semantics _ _ _ _ _ _ _ _ _))))). assumption. left; reflexivity. right; left; reflexivity. intros. rewrite (config_OK_zero cfg H) in H0. discriminate. intros. rewrite (config_OK_one cfg H) in H0. discriminate. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2 bdd6 bdd7 BDDdummy_lemma_2 BDDdummy_lemma_3 BDDdummy_lemma_4 bdd8 bdd9 bdd10