proposition: Lemma bool_fun_if_lemma_3 : forall (x : BDDvar) (bf1 bfl2 bfr2 : bool_fun), bool_fun_eq (bool_fun_if x (bool_fun_or bf1 bfr2) (bool_fun_or bf1 bfl2)) (bool_fun_or bf1 (bool_fun_if x bfr2 bfl2)).
proof: Proof. unfold bool_fun_eq, bool_fun_or, bool_fun_if in |- *. unfold bool_fun_eval in |- *. intros x bf1 bfl2 bfr2 vb. elim (vb x); simpl in |- *. reflexivity. 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