proposition: Lemma bool_fun_eq_symm : forall bf1 bf2 : bool_fun, bool_fun_eq bf1 bf2 -> bool_fun_eq bf2 bf1.
proof: Proof. unfold bool_fun_eq in |- *. unfold bool_fun_eval in |- *. intros bf1 bf2 H vb. rewrite (H vb). reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1