proposition: Lemma bool_fun_restrict_one : forall (x : BDDvar) (b : bool), bool_fun_eq (bool_fun_restrict bool_fun_one x b) bool_fun_one.
proof: Proof. intros x b. unfold bool_fun_eq, bool_fun_restrict, bool_fun_zero, bool_fun_one in |- *. intros vb. unfold bool_fun_eval, augment in |- *. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2