proposition: Lemma bool_fun_eq_lemma : forall (bf1 bf2 : bool_fun) (x : BDDvar), bool_fun_ext bf1 -> bool_fun_ext bf2 -> bool_fun_eq (bool_fun_restrict bf1 x true) (bool_fun_restrict bf2 x true) -> bool_fun_eq (bool_fun_restrict bf1 x false) (bool_fun_restrict bf2 x false) -> bool_fun_eq bf1 bf2.
proof: Proof. intros bf1 bf2 x H H0 H1 H2. unfold bool_fun_eq in |- *. intro vb. elim (sumbool_of_bool (vb x)); intro. cut (var_binding_eq (augment vb x true) vb). intro H3. cut (bool_fun_eval bf2 (augment vb x true) = bool_fun_eval bf2 vb). cut (bool_fun_eval bf1 (augment vb x true) = bool_fun_eval bf1 vb). intros H4 H5. rewrite <- H4. rewrite <- H5. unfold bool_fun_eq, bool_fun_restrict in H1. unfold bool_fun_eval at 1 3 in H1. apply H1. apply H. assumption. apply H0. assumption. apply augment_eq. assumption. cut (var_binding_eq (augment vb x false) vb). intro H3. cut (bool_fun_eval bf2 (augment vb x false) = bool_fun_eval bf2 vb). cut (bool_fun_eval bf1 (augment vb x false) = bool_fun_eval bf1 vb). intros H4 H5. rewrite <- H4. rewrite <- H5. unfold bool_fun_eq, bool_fun_restrict in H2. unfold bool_fun_eval at 1 3 in H2. apply H2. apply H. assumption. apply H0. assumption. apply augment_eq. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2