proposition: Lemma bool_fun_independent_lemma : forall (bf : bool_fun) (x : BDDvar) (vb : var_binding) (b : bool), bool_fun_ext bf -> bool_fun_independent bf x -> bool_fun_eval bf (augment vb x b) = bool_fun_eval bf vb.
proof: Proof. intros bf x vb b H H0. elim (sumbool_of_bool (vb x)). intro y. elim b. cut (var_binding_eq (augment vb x true) vb). intro H1. rewrite (H (augment vb x true) vb H1). cut (bool_fun_eval bf (augment vb x true) = bool_fun_eval bf vb). unfold bool_fun_eval in |- *. intro H2. reflexivity. rewrite (H (augment vb x true) vb H1). reflexivity. apply augment_eq. assumption. rewrite <- (H0 vb). cut (var_binding_eq (augment vb x true) vb). intro H1. rewrite (H (augment vb x true) vb H1). cut (bool_fun_eval bf (augment vb x true) = bool_fun_eval bf vb). unfold bool_fun_eval in |- *. intro H2. reflexivity. rewrite (H (augment vb x true) vb H1). reflexivity. apply augment_eq. assumption. intro y. elim b. cut (var_binding_eq (augment vb x false) vb). intro H1. cut (bool_fun_eval bf (augment vb x false) = bool_fun_eval bf vb). intro H2. rewrite <- H2. apply H0. apply H. assumption. apply augment_eq. assumption. cut (var_binding_eq (augment vb x false) vb). intro H1. apply H. assumption. apply augment_eq. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2