proposition: Lemma bool_fun_restrict_neg_1 : forall (bf : bool_fun) (x : BDDvar) (b : bool), bool_fun_ext bf -> bool_fun_eq (bool_fun_restrict (bool_fun_neg bf) x b) (bool_fun_neg (bool_fun_restrict bf x b)).
proof: Proof. intros bf x b H. unfold bool_fun_eq in |- *. unfold bool_fun_restrict in |- *. unfold bool_fun_eval at 2 in |- *. intro vb. unfold bool_fun_neg in |- *. unfold bool_fun_eval at 3 in |- *. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4