proposition: Lemma bool_fun_and_preserves_eq : forall bf1 bf2 bf1' bf2' : bool_fun, bool_fun_eq bf1 bf1' -> bool_fun_eq bf2 bf2' -> bool_fun_eq (bool_fun_and bf1 bf2) (bool_fun_and bf1' bf2').
proof: Proof. intros. unfold bool_fun_eq in H, H0. unfold bool_fun_eval in H, H0. unfold bool_fun_eq, bool_fun_and in |- *. unfold bool_fun_eval in |- *. intro. rewrite (H vb). rewrite (H0 vb). reflexivity. 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