proposition: Lemma bool_fun_if_preserves_eq : forall (x : BDDvar) (bf1 bf2 bf1' bf2' : bool_fun), bool_fun_eq bf1 bf1' -> bool_fun_eq bf2 bf2' -> bool_fun_eq (bool_fun_if x bf1 bf2) (bool_fun_if x bf1' bf2').
proof: Proof. unfold bool_fun_eq, bool_fun_if in |- *. unfold bool_fun_eval in |- *. intros x bf1 bf2 bf1' bf2' H H0 vb. 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