proposition: Lemma bool_fun_or_commute : forall bf bf' : bool_fun, bool_fun_eq (bool_fun_or bf bf') (bool_fun_or bf' bf).
proof: Proof. unfold bool_fun_eq, bool_fun_or in |- *. unfold bool_fun_eval, bool_fun_or in |- *. intros bf bf' vb. apply orb_comm. 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