(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Require Import Bool.
Require Import Sumbool.
Require Import Arith.
Require Import ZArith NArith Nnat Ndec Ndigits.
From IntMap Require Import Allmaps.
Require Import List.
Require Import Wf_nat.

Require Import misc.
Require Import bool_fun.
Require Import myMap.
Require Import config.
Require Import alloc.
Require Import make.
Require Import neg.
Require Import or.
Require Import op.

Section tauto.

Variable gc : BDDconfig -> list ad -> BDDconfig.
Hypothesis gc_is_OK : gc_OK gc.

Fixpoint BDDof_bool_expr (cfg : BDDconfig) (ul : list ad) 
 (be : bool_expr) {struct be} : BDDconfig * ad :=
  match be with
  | Zero => (cfg, BDDzero)
  | One => (cfg, BDDone)
  | Var x => BDDvar_make gc cfg ul x
  | Neg be1 =>
      match BDDof_bool_expr cfg ul be1 with
      | (cfg1, node1) => BDDneg gc cfg1 (node1 :: ul) node1
      end
  | Or be1 be2 =>
      match BDDof_bool_expr cfg ul be1 with
      | (cfg1, node1) =>
          match BDDof_bool_expr cfg1 (node1 :: ul) be2 with
          | (cfg2, node2) => BDDor gc cfg2 (node2 :: node1 :: ul) node1 node2
          end
      end
  | ANd be1 be2 =>
      match BDDof_bool_expr cfg ul be1 with
      | (cfg1, node1) =>
          match BDDof_bool_expr cfg1 (node1 :: ul) be2 with
          | (cfg2, node2) =>
              BDDand gc cfg2 (node2 :: node1 :: ul) node1 node2
          end
      end
  | Impl be1 be2 =>
      match BDDof_bool_expr cfg ul be1 with
      | (cfg1, node1) =>
          match BDDof_bool_expr cfg1 (node1 :: ul) be2 with
          | (cfg2, node2) =>
              BDDimpl gc cfg2 (node2 :: node1 :: ul) node1 node2
          end
      end
  | Iff be1 be2 =>
      match BDDof_bool_expr cfg ul be1 with
      | (cfg1, node1) =>
          match BDDof_bool_expr cfg1 (node1 :: ul) be2 with
          | (cfg2, node2) =>
              BDDiff gc cfg2 (node2 :: node1 :: ul) node1 node2
          end
      end
  end.

Lemma BDDof_bool_expr_correct :
 forall (be : bool_expr) (cfg : BDDconfig) (ul : list ad),
 BDDconfig_OK cfg ->
 used_list_OK cfg ul ->
 BDDconfig_OK (fst (BDDof_bool_expr cfg ul be)) /\
 used_nodes_preserved cfg (fst (BDDof_bool_expr cfg ul be)) ul /\
 config_node_OK (fst (BDDof_bool_expr cfg ul be))
   (snd (BDDof_bool_expr cfg ul be)) /\
 bool_fun_eq
   (bool_fun_of_BDD (fst (BDDof_bool_expr cfg ul be))
      (snd (BDDof_bool_expr cfg ul be))) (bool_fun_of_bool_expr be).
Proof.
(* Goal: forall (be : bool_expr) (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul be))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul be)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul be)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul be))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul be)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul be))) (bool_fun_of_bool_expr be)))) *)
  simple induction be.  intros.  simpl in |- *.  split.  assumption.  split.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_nodes_preserved_refl.  split.  apply zero_OK.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  apply bool_fun_of_BDD_zero.  assumption.  intros.  simpl in |- *.  split.  assumption.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  split.  apply used_nodes_preserved_refl.  split.  apply one_OK.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  apply bool_fun_of_BDD_one.  assumption.  intros.  simpl in |- *.  split.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDvar_make_config_OK.  assumption.  assumption.  assumption.  split.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDvar_make_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  split.  apply BDDvar_make_node_OK.  assumption.  assumption.  assumption.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  apply BDDvar_make_is_var.  assumption.  assumption.  assumption.  intros.
(* Goal: forall (node : ad) (_ : @In ad node (@nil ad)), node_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) cfg) node *)
  simpl in |- *.
(* Goal: forall (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b))) (_ : and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_of_bool_expr b)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
  elim (prod_sum _ _ (BDDof_bool_expr cfg ul b)).  intros cfg1 H2.  elim H2.
(* Goal: forall (x : ad) (_ : @eq (prod BDDconfig ad) (BDDof_bool_expr cfg ul b) (@pair BDDconfig ad cfg1 x)), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in BDDneg gc cfg1 (@cons ad node1 ul) node1))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in BDDneg gc cfg1 (@cons ad node1 ul) node1)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in BDDneg gc cfg1 (@cons ad node1 ul) node1)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in BDDneg gc cfg1 (@cons ad node1 ul) node1))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in BDDneg gc cfg1 (@cons ad node1 ul) node1)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in BDDneg gc cfg1 (@cons ad node1 ul) node1))) (bool_fun_neg (bool_fun_of_bool_expr b))))) *)
(* Goal: forall (b : bool_expr) (_ : forall (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_of_bool_expr b))))) (b0 : bool_expr) (_ : forall (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b0))) (bool_fun_of_bool_expr b0))))) (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Or b b0)))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Or b b0))) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Or b b0))) (@snd BDDconfig ad (BDDof_bool_expr cfg ul (Or b b0)))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Or b b0))) (@snd BDDconfig ad (BDDof_bool_expr cfg ul (Or b b0)))) (bool_fun_of_bool_expr (Or b b0))))) *)
(* Goal: forall (b : bool_expr) (_ : forall (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_of_bool_expr b))))) (b0 : bool_expr) (_ : forall (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b0))) (bool_fun_of_bool_expr b0))))) (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul (ANd b b0)))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul (ANd b b0))) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul (ANd b b0))) (@snd BDDconfig ad (BDDof_bool_expr cfg ul (ANd b b0)))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul (ANd b b0))) (@snd BDDconfig ad (BDDof_bool_expr cfg ul (ANd b b0)))) (bool_fun_of_bool_expr (ANd b b0))))) *)
(* Goal: forall (b : bool_expr) (_ : forall (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_of_bool_expr b))))) (b0 : bool_expr) (_ : forall (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b0))) (bool_fun_of_bool_expr b0))))) (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Impl b b0)))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Impl b b0))) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Impl b b0))) (@snd BDDconfig ad (BDDof_bool_expr cfg ul (Impl b b0)))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Impl b b0))) (@snd BDDconfig ad (BDDof_bool_expr cfg ul (Impl b b0)))) (bool_fun_of_bool_expr (Impl b b0))))) *)
(* Goal: forall (b : bool_expr) (_ : forall (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_of_bool_expr b))))) (b0 : bool_expr) (_ : forall (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b0))) (bool_fun_of_bool_expr b0))))) (cfg : BDDconfig) (ul : list ad) (_ : BDDconfig_OK cfg) (_ : used_list_OK cfg ul), and (BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Iff b b0)))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Iff b b0))) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Iff b b0))) (@snd BDDconfig ad (BDDof_bool_expr cfg ul (Iff b b0)))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul (Iff b b0))) (@snd BDDconfig ad (BDDof_bool_expr cfg ul (Iff b b0)))) (bool_fun_of_bool_expr (Iff b b0))))) *)
  clear H2.  intros node1 H2.  rewrite H2.  elim (H cfg ul H0 H1).  clear H.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  rewrite H2.  simpl in |- *.  intros.  elim H3; clear H3; intros.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  elim H4; clear H4; intros.  cut (used_list_OK cfg1 (node1 :: ul)).  intro.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  cut (used_node' cfg1 (node1 :: ul) node1).  intro.  split.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  split.  apply used_nodes_preserved_trans with (cfg2 := cfg1).  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply used_nodes_preserved_cons with (node := node1).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.  
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  split.  apply BDDneg_node_OK.  assumption.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  
  apply
   bool_fun_eq_trans with (bf2 := bool_fun_neg (bool_fun_of_BDD cfg1 node1)).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDneg_is_neg.  assumption.  assumption.  assumption.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply bool_fun_neg_preserves_eq.  assumption.  apply used_node'_cons_node_ul.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply node_OK_list_OK.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_nodes_preserved_list_OK with (cfg := cfg).  assumption.  assumption.



(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  intros.  simpl in |- *.  elim (H cfg ul H1 H2).  clear H.
(* Goal: forall (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b))) (_ : and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_of_bool_expr b)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
  elim (prod_sum _ _ (BDDof_bool_expr cfg ul b)).  intros cfg1 H3.  elim H3.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  clear H3.  intros node1 H3.  rewrite H3.  simpl in |- *.  intros.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  elim H4; clear H4; intros.  elim H5; clear H5; intros.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_list_OK cfg1 ul *)
  cut (used_list_OK cfg1 ul).  intro.  cut (used_list_OK cfg1 (node1 :: ul)).
(* Goal: forall _ : bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be), @eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  intro.  cut (used_node' cfg1 (node1 :: ul) node1).  intro.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  elim (H0 cfg1 (node1 :: ul) H H8).  clear H0.
(* Goal: forall (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (_ : and (used_nodes_preserved cfg1 (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@cons ad node1 ul)) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_of_bool_expr b0)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  elim (prod_sum _ _ (BDDof_bool_expr cfg1 (node1 :: ul) b0)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0) (@pair BDDconfig ad x b))) (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (_ : and (used_nodes_preserved cfg1 (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@cons ad node1 ul)) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_of_bool_expr b0)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  intros cfg2 H10.  elim H10.  clear H10.  intros node2 H10.  rewrite H10.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  simpl in |- *.  intros.  elim H11; clear H11; intros.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  elim H12; clear H12; intros.  cut (used_list_OK cfg2 (node1 :: ul)).
(* Goal: forall _ : bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be), @eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  intro.  cut (used_list_OK cfg2 (node2 :: node1 :: ul)).  intro.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  cut (used_node' cfg2 (node2 :: node1 :: ul) node2).
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  cut (used_node' cfg2 (node2 :: node1 :: ul) node1).  intros.  split.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDor_config_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  split.  apply used_nodes_preserved_trans with (cfg2 := cfg1).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  apply used_nodes_preserved_cons with (node := node1).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_nodes_preserved_trans with (cfg2 := cfg2).  assumption.  assumption.
(* Goal: used_nodes_preserved cfg2 (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@cons ad node1 ul) *)
(* Goal: and (config_node_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))) *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node2 *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply used_nodes_preserved_cons with (node := node2).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDor_used_nodes_preserved.  assumption.  assumption.  assumption.  
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  split.  apply BDDor_node_OK.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  assumption.  assumption.
  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_or (bool_fun_of_BDD cfg2 node1)
                (bool_fun_of_BDD cfg2 node2)).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDor_is_or.  assumption.  assumption.  assumption.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply bool_fun_or_preserves_eq.
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node1) (bool_fun_of_bool_expr b) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node2) (bool_fun_of_bool_expr b0) *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node2 *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg1 node1).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_nodes_preserved'_bool_fun with (ul := node1 :: ul).  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  assumption.  assumption.  assumption.  assumption.
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply used_node'_cons_node'_ul.  apply used_node'_cons_node_ul.  
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_node'_cons_node_ul.  apply node_OK_list_OK.  assumption.  
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply used_nodes_preserved_list_OK with (cfg := cfg1).  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply used_node'_cons_node_ul.  apply node_OK_list_OK.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  apply used_nodes_preserved_list_OK with (cfg := cfg).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  


(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  intros.  simpl in |- *.  elim (H cfg ul H1 H2).  clear H.
(* Goal: forall (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b))) (_ : and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_of_bool_expr b)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
  elim (prod_sum _ _ (BDDof_bool_expr cfg ul b)).  intros cfg1 H3.  elim H3.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  clear H3.  intros node1 H3.  rewrite H3.  simpl in |- *.  intros.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  elim H4; clear H4; intros.  elim H5; clear H5; intros.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_list_OK cfg1 ul *)
  cut (used_list_OK cfg1 ul).  intro.  cut (used_list_OK cfg1 (node1 :: ul)).
(* Goal: forall _ : bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be), @eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  intro.  cut (used_node' cfg1 (node1 :: ul) node1).  intro.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  elim (H0 cfg1 (node1 :: ul) H H8).  clear H0.
(* Goal: forall (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (_ : and (used_nodes_preserved cfg1 (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@cons ad node1 ul)) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_of_bool_expr b0)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  elim (prod_sum _ _ (BDDof_bool_expr cfg1 (node1 :: ul) b0)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0) (@pair BDDconfig ad x b))) (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (_ : and (used_nodes_preserved cfg1 (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@cons ad node1 ul)) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_of_bool_expr b0)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  intros cfg2 H10.  elim H10.  clear H10.  intros node2 H10.  rewrite H10.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  simpl in |- *.  intros.  elim H11; clear H11; intros.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  elim H12; clear H12; intros.  cut (used_list_OK cfg2 (node1 :: ul)).
(* Goal: forall _ : bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be), @eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  intro.  cut (used_list_OK cfg2 (node2 :: node1 :: ul)).  intro.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  cut (used_node' cfg2 (node2 :: node1 :: ul) node2).
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  cut (used_node' cfg2 (node2 :: node1 :: ul) node1).  intros.  split.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDand_config_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  split.  apply used_nodes_preserved_trans with (cfg2 := cfg1).  
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  apply used_nodes_preserved_cons with (node := node1).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_nodes_preserved_trans with (cfg2 := cfg2).  assumption.  assumption.
(* Goal: used_nodes_preserved cfg2 (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@cons ad node1 ul) *)
(* Goal: and (config_node_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))) *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node2 *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply used_nodes_preserved_cons with (node := node2).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDand_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  split.  apply BDDand_node_OK.  assumption.  
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  assumption.  assumption.
  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_and (bool_fun_of_BDD cfg2 node1)
                (bool_fun_of_BDD cfg2 node2)).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDand_is_and.  assumption.  assumption.  assumption.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply bool_fun_and_preserves_eq.
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node1) (bool_fun_of_bool_expr b) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node2) (bool_fun_of_bool_expr b0) *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node2 *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg1 node1).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_nodes_preserved'_bool_fun with (ul := node1 :: ul).  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  assumption.  assumption.  assumption.  assumption.
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply used_node'_cons_node'_ul.  apply used_node'_cons_node_ul.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_node'_cons_node_ul.  apply node_OK_list_OK.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply used_nodes_preserved_list_OK with (cfg := cfg1).  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply used_node'_cons_node_ul.  apply node_OK_list_OK.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  apply used_nodes_preserved_list_OK with (cfg := cfg).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.

(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  intros.  simpl in |- *.  elim (H cfg ul H1 H2).  clear H.
(* Goal: forall (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b))) (_ : and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_of_bool_expr b)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
  elim (prod_sum _ _ (BDDof_bool_expr cfg ul b)).  intros cfg1 H3.  elim H3.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  clear H3.  intros node1 H3.  rewrite H3.  simpl in |- *.  intros.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  elim H4; clear H4; intros.  elim H5; clear H5; intros.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_list_OK cfg1 ul *)
  cut (used_list_OK cfg1 ul).  intro.  cut (used_list_OK cfg1 (node1 :: ul)).
(* Goal: forall _ : bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be), @eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  intro.  cut (used_node' cfg1 (node1 :: ul) node1).  intro.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  elim (H0 cfg1 (node1 :: ul) H H8).  clear H0.
(* Goal: forall (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (_ : and (used_nodes_preserved cfg1 (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@cons ad node1 ul)) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_of_bool_expr b0)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  elim (prod_sum _ _ (BDDof_bool_expr cfg1 (node1 :: ul) b0)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0) (@pair BDDconfig ad x b))) (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (_ : and (used_nodes_preserved cfg1 (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@cons ad node1 ul)) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_of_bool_expr b0)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  intros cfg2 H10.  elim H10.  clear H10.  intros node2 H10.  rewrite H10.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  simpl in |- *.  intros.  elim H11; clear H11; intros.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  elim H12; clear H12; intros.  cut (used_list_OK cfg2 (node1 :: ul)).
(* Goal: forall _ : bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be), @eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  intro.  cut (used_list_OK cfg2 (node2 :: node1 :: ul)).  intro.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  cut (used_node' cfg2 (node2 :: node1 :: ul) node2).
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  cut (used_node' cfg2 (node2 :: node1 :: ul) node1).  intros.  split.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDimpl_config_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  split.  apply used_nodes_preserved_trans with (cfg2 := cfg1).  
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  apply used_nodes_preserved_cons with (node := node1).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_nodes_preserved_trans with (cfg2 := cfg2).  assumption.  assumption.
(* Goal: used_nodes_preserved cfg2 (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@cons ad node1 ul) *)
(* Goal: and (config_node_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))) *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node2 *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply used_nodes_preserved_cons with (node := node2).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDimpl_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  split.  apply BDDimpl_node_OK.  assumption.  
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  assumption.  assumption.
  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_impl (bool_fun_of_BDD cfg2 node1)
                (bool_fun_of_BDD cfg2 node2)).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDimpl_is_impl.  assumption.  assumption.  assumption.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply bool_fun_impl_preserves_eq.
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node1) (bool_fun_of_bool_expr b) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node2) (bool_fun_of_bool_expr b0) *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node2 *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg1 node1).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_nodes_preserved'_bool_fun with (ul := node1 :: ul).  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  assumption.  assumption.  assumption.  assumption.
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply used_node'_cons_node'_ul.  apply used_node'_cons_node_ul.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_node'_cons_node_ul.  apply node_OK_list_OK.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply used_nodes_preserved_list_OK with (cfg := cfg1).  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply used_node'_cons_node_ul.  apply node_OK_list_OK.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  apply used_nodes_preserved_list_OK with (cfg := cfg).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.


(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  intros.  simpl in |- *.  elim (H cfg ul H1 H2).  clear H.
(* Goal: forall (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b))) (_ : and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg ul b)) (@snd BDDconfig ad (BDDof_bool_expr cfg ul b))) (bool_fun_of_bool_expr b)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg1, node1) := BDDof_bool_expr cfg ul b in let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
  elim (prod_sum _ _ (BDDof_bool_expr cfg ul b)).  intros cfg1 H3.  elim H3.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  clear H3.  intros node1 H3.  rewrite H3.  simpl in |- *.  intros.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  elim H4; clear H4; intros.  elim H5; clear H5; intros.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_list_OK cfg1 ul *)
  cut (used_list_OK cfg1 ul).  intro.  cut (used_list_OK cfg1 (node1 :: ul)).
(* Goal: forall _ : bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be), @eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  intro.  cut (used_node' cfg1 (node1 :: ul) node1).  intro.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  elim (H0 cfg1 (node1 :: ul) H H8).  clear H0.
(* Goal: forall (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (_ : and (used_nodes_preserved cfg1 (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@cons ad node1 ul)) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_of_bool_expr b0)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  elim (prod_sum _ _ (BDDof_bool_expr cfg1 (node1 :: ul) b0)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0) (@pair BDDconfig ad x b))) (_ : BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (_ : and (used_nodes_preserved cfg1 (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@cons ad node1 ul)) (and (config_node_OK (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0)) (@snd BDDconfig ad (BDDof_bool_expr cfg1 (@cons ad node1 ul) b0))) (bool_fun_of_bool_expr b0)))), and (BDDconfig_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (let (cfg2, node2) := BDDof_bool_expr cfg1 (@cons ad node1 ul) b0 in BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  intros cfg2 H10.  elim H10.  clear H10.  intros node2 H10.  rewrite H10.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  simpl in |- *.  intros.  elim H11; clear H11; intros.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  elim H12; clear H12; intros.  cut (used_list_OK cfg2 (node1 :: ul)).
(* Goal: forall _ : bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be), @eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  intro.  cut (used_list_OK cfg2 (node2 :: node1 :: ul)).  intro.
(* Goal: and (BDDconfig_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (and (used_nodes_preserved cfg (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) ul) (and (config_node_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))))) *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  cut (used_node' cfg2 (node2 :: node1 :: ul) node2).
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  cut (used_node' cfg2 (node2 :: node1 :: ul) node1).  intros.  split.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDiff_config_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  split.  apply used_nodes_preserved_trans with (cfg2 := cfg1).  
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  apply used_nodes_preserved_cons with (node := node1).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_nodes_preserved_trans with (cfg2 := cfg2).  assumption.  assumption.
(* Goal: used_nodes_preserved cfg2 (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@cons ad node1 ul) *)
(* Goal: and (config_node_OK (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2)) (@snd BDDconfig ad (BDDiff gc cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 node2))) (bool_fun_iff (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0))) *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node2 *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply used_nodes_preserved_cons with (node := node2).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDiff_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  split.  apply BDDiff_node_OK.  assumption.  
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  assumption.  assumption.
  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_iff (bool_fun_of_BDD cfg2 node1)
                (bool_fun_of_BDD cfg2 node2)).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDiff_is_iff.  assumption.  assumption.  assumption.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply bool_fun_iff_preserves_eq.
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node1) (bool_fun_of_bool_expr b) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node2) (bool_fun_of_bool_expr b0) *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node1 *)
(* Goal: used_node' cfg2 (@cons ad node2 (@cons ad node1 ul)) node2 *)
(* Goal: used_list_OK cfg2 (@cons ad node2 (@cons ad node1 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node1 ul) *)
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg1 node1).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_nodes_preserved'_bool_fun with (ul := node1 :: ul).  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  assumption.  assumption.  assumption.  assumption.
(* Goal: used_node' cfg1 (@cons ad node1 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node1 ul) *)
(* Goal: used_list_OK cfg1 ul *)
  apply used_node'_cons_node'_ul.  apply used_node'_cons_node_ul.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply used_node'_cons_node_ul.  apply node_OK_list_OK.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply used_nodes_preserved_list_OK with (cfg := cfg1).  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  apply used_node'_cons_node_ul.  apply node_OK_list_OK.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.  apply used_nodes_preserved_list_OK with (cfg := cfg).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  assumption.  assumption.
Qed.

Lemma init_list_OK : forall cfg : BDDconfig, used_list_OK cfg nil.
Proof.
(* Goal: forall (node : ad) (_ : @In ad node (@nil ad)), node_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) cfg) node *)
  intro.  unfold used_list_OK in |- *.  unfold used_list_OK_bs in |- *.  simpl in |- *.  tauto.
Qed.

Definition is_tauto (be : bool_expr) :=
  Neqb BDDone (snd (BDDof_bool_expr initBDDconfig nil be)).

Lemma is_tauto_lemma :
 forall be : bool_expr,
 is_tauto be = true <-> bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be).
Proof.
(* Goal: forall be : bool_expr, iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
  unfold is_tauto in |- *.  intros.
  cut
   (bool_fun_eq
      (bool_fun_of_BDD (fst (BDDof_bool_expr initBDDconfig nil be))
         (snd (BDDof_bool_expr initBDDconfig nil be)))
      (bool_fun_of_bool_expr be)).
(* Goal: iff (@eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true) (bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  intro.  split.  intro.  rewrite <- (Neqb_complete _ _ H0) in H.
  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_of_BDD (fst (BDDof_bool_expr initBDDconfig nil be))
                BDDone).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) BDDone) bool_fun_one *)
(* Goal: bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_bool_expr be) (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply bool_fun_eq_sym.  apply bool_fun_of_BDD_one.
(* Goal: BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) *)
(* Goal: bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_bool_expr be) (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  refine (proj1 (BDDof_bool_expr_correct _ _ _ _ _)).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply initBDDconfig_OK.  apply init_list_OK.  assumption.  intro.
(* Goal: @eq bool (N.eqb BDDone (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) true *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply BDDunique with (cfg := fst (BDDof_bool_expr initBDDconfig nil be)).
(* Goal: BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) *)
(* Goal: bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_bool_expr be) (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  refine (proj1 (BDDof_bool_expr_correct _ _ _ _ _)).
(* Goal: config_node_OK (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) BDDone *)
(* Goal: config_node_OK (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) BDDone) (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply initBDDconfig_OK.  apply init_list_OK.  apply one_OK.
(* Goal: config_node_OK (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) BDDone) (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  refine (proj1 (proj2 (proj2 (BDDof_bool_expr_correct _ _ _ _ _)))).
(* Goal: BDDconfig_OK initBDDconfig *)
(* Goal: used_list_OK initBDDconfig (@nil ad) *)
  apply initBDDconfig_OK.  apply init_list_OK.  
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) BDDone) (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply bool_fun_eq_trans with (bf2 := bool_fun_of_bool_expr be).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) BDDone) bool_fun_one *)
(* Goal: bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_bool_expr be) (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply bool_fun_eq_trans with (bf2 := bool_fun_one).  apply bool_fun_of_BDD_one.
(* Goal: BDDconfig_OK (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) *)
(* Goal: bool_fun_eq bool_fun_one (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_bool_expr be) (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  refine (proj1 (BDDof_bool_expr_correct _ _ _ _ _)).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply initBDDconfig_OK.  apply init_list_OK.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  apply bool_fun_eq_sym.  assumption.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be)) (@snd BDDconfig ad (BDDof_bool_expr initBDDconfig (@nil ad) be))) (bool_fun_of_bool_expr be) *)
  refine (proj2 (proj2 (proj2 (BDDof_bool_expr_correct _ _ _ _ _)))).
(* Goal: BDDconfig_OK initBDDconfig *)
(* Goal: used_list_OK initBDDconfig (@nil ad) *)
  apply initBDDconfig_OK.  apply init_list_OK.  
Qed.

(* Goal: forall (node : ad) (_ : False), node_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) cfg) node *)
End tauto.