(* 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 Map.
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.

Section BDDop.

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


                         Section BDDneg_results.

Variable cfg : BDDconfig.
Variable ul : list ad.
Variable node : ad.

Hypothesis cfg_OK : BDDconfig_OK cfg.
Hypothesis ul_OK : used_list_OK cfg ul.
Hypothesis used : used_node' cfg ul node.

Definition BDDneg :=
  BDDneg_1 gc cfg ul node (S (nat_of_N (node_height cfg node))).

Let lt_1 :
  nat_of_N (node_height cfg node) < S (nat_of_N (node_height cfg node)).
Proof.
(* Goal: lt (N.to_nat (node_height cfg node)) (S (N.to_nat (node_height cfg node))) *)
  unfold lt in |- *.  apply le_n.
Qed.

Lemma BDDneg_config_OK : BDDconfig_OK (fst BDDneg).
Proof.
(* Goal: @eq bool (N.eqb (node_height (@fst BDDconfig ad BDDneg) (@snd BDDconfig ad BDDneg)) (node_height cfg node)) true *)
  unfold BDDneg in |- *.
  exact
   (proj1
      (BDDneg_1_lemma gc gc_is_OK (S (nat_of_N (node_height cfg node))) cfg
         ul node lt_1 cfg_OK ul_OK used)).
Qed.

Lemma BDDneg_node_OK : config_node_OK (fst BDDneg) (snd BDDneg).
Proof.
(* Goal: @eq bool (N.eqb (node_height (@fst BDDconfig ad BDDneg) (@snd BDDconfig ad BDDneg)) (node_height cfg node)) true *)
  unfold BDDneg in |- *.
  exact
   (proj1
      (proj2
         (BDDneg_1_lemma gc gc_is_OK (S (nat_of_N (node_height cfg node)))
            cfg ul node lt_1 cfg_OK ul_OK used))).
Qed.

Lemma BDDneg_used_nodes_preserved : used_nodes_preserved cfg (fst BDDneg) ul.
Proof.
(* Goal: @eq bool (N.eqb (node_height (@fst BDDconfig ad BDDneg) (@snd BDDconfig ad BDDneg)) (node_height cfg node)) true *)
  unfold BDDneg in |- *.
  exact
   (proj1
      (proj2
         (proj2
            (BDDneg_1_lemma gc gc_is_OK
               (S (nat_of_N (node_height cfg node))) cfg ul node lt_1 cfg_OK
               ul_OK used)))).
Qed.

Lemma BDDneg_is_neg :
 bool_fun_eq (bool_fun_of_BDD (fst BDDneg) (snd BDDneg))
   (bool_fun_neg (bool_fun_of_BDD cfg node)).
Proof.
(* Goal: @eq bool (N.eqb (node_height (@fst BDDconfig ad BDDneg) (@snd BDDconfig ad BDDneg)) (node_height cfg node)) true *)
  unfold BDDneg in |- *.
  exact
   (proj2
      (proj2
         (proj2
            (proj2
               (BDDneg_1_lemma gc gc_is_OK
                  (S (nat_of_N (node_height cfg node))) cfg ul node lt_1
                  cfg_OK ul_OK used))))).
Qed.

Lemma BDDneg_list_OK : used_list_OK (fst BDDneg) ul.
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) ul *)
  apply used_nodes_preserved_list_OK with (cfg := cfg).  assumption.
(* Goal: used_nodes_preserved cfg (@fst BDDconfig ad BDDneg) ul *)
  exact BDDneg_used_nodes_preserved.  
Qed.

Lemma BDDneg_list_OK_cons : used_list_OK (fst BDDneg) (snd BDDneg :: ul).
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.  exact BDDneg_node_OK.  exact BDDneg_list_OK.
Qed.

Lemma BDDneg_var_eq :
 Neqb (node_height (fst BDDneg) (snd BDDneg)) (node_height cfg node) = true.
Proof.
(* Goal: @eq bool (N.eqb (node_height (@fst BDDconfig ad BDDneg) (@snd BDDconfig ad BDDneg)) (node_height cfg node)) true *)
  unfold BDDneg in |- *.
  exact
   (proj1
      (proj2
         (proj2
            (proj2
               (BDDneg_1_lemma gc gc_is_OK
                  (S (nat_of_N (node_height cfg node))) cfg ul node lt_1
                  cfg_OK ul_OK used))))).
Qed.

                         End BDDneg_results.


                        Section BDDor_results.


Variable cfg : BDDconfig.
Variable ul : list ad.
Variable node1 node2 : ad.

Hypothesis cfg_OK : BDDconfig_OK cfg.
Hypothesis ul_OK : used_list_OK cfg ul.
Hypothesis used1 : used_node' cfg ul node1.
Hypothesis used2 : used_node' cfg ul node2.

Definition BDDor :=
  BDDor_1 gc cfg ul node1 node2
    (S
       (max (nat_of_N (node_height cfg node1))
          (nat_of_N (node_height cfg node2)))).
Let lt_1 :
  max (nat_of_N (node_height cfg node1)) (nat_of_N (node_height cfg node2)) <
  S
    (max (nat_of_N (node_height cfg node1))
       (nat_of_N (node_height cfg node2))).
Proof.
(* Goal: lt (N.to_nat (node_height cfg node)) (S (N.to_nat (node_height cfg node))) *)
  unfold lt in |- *.  apply le_n.
Qed.

Lemma BDDor_config_OK : BDDconfig_OK (fst BDDor).
Proof.
  exact
   (proj1 (BDDor_1_lemma _ gc_is_OK _ _ _ _ _ lt_1 cfg_OK ul_OK used1 used2)).
Qed.

Lemma BDDor_node_OK : config_node_OK (fst BDDor) (snd BDDor).
Proof.
  exact
   (proj1
      (proj2
         (BDDor_1_lemma _ gc_is_OK _ _ _ _ _ lt_1 cfg_OK ul_OK used1 used2))).
Qed.

Lemma BDDor_used_nodes_preserved : used_nodes_preserved cfg (fst BDDor) ul.
Proof.
  exact
   (proj1
      (proj2
         (proj2
            (BDDor_1_lemma _ gc_is_OK _ _ _ _ _ lt_1 cfg_OK ul_OK used1 used2)))).
Qed.

Lemma BDDor_is_or :
 bool_fun_eq (bool_fun_of_BDD (fst BDDor) (snd BDDor))
   (bool_fun_or (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)).
Proof.
  exact
   (proj2
      (proj2
         (proj2
            (proj2
               (BDDor_1_lemma _ gc_is_OK _ _ _ _ _ lt_1 cfg_OK ul_OK used1
                  used2))))).
Qed.

Lemma BDDor_list_OK : used_list_OK (fst BDDor) ul.
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) ul *)
  apply used_nodes_preserved_list_OK with (cfg := cfg).  assumption.
(* Goal: used_nodes_preserved cfg (@fst BDDconfig ad BDDor) ul *)
  exact BDDor_used_nodes_preserved.
Qed.

Lemma BDDor_list_OK_cons : used_list_OK (fst BDDor) (snd BDDor :: ul).
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.  exact BDDor_node_OK.  exact BDDor_list_OK.
Qed.

Lemma BDDor_var_le :
 Nleb (node_height (fst BDDor) (snd BDDor))
   (BDDvar_max (node_height cfg node1) (node_height cfg node2)) = true.
Proof.
  exact
   (proj1
      (proj2
         (proj2
            (proj2
               (BDDor_1_lemma _ gc_is_OK _ _ _ _ _ lt_1 cfg_OK ul_OK used1
                  used2))))).
Qed.

                          End BDDor_results.



                       Section BDDimpl_results.



Variable cfg : BDDconfig.
Variable ul : list ad.
Variable node1 node2 : ad.

Hypothesis cfg_OK : BDDconfig_OK cfg.
Hypothesis ul_OK : used_list_OK cfg ul.
Hypothesis used1 : used_node' cfg ul node1.
Hypothesis used2 : used_node' cfg ul node2.

Definition BDDimpl :=
  match BDDneg cfg ul node1 with
  | (cfg1, node1') => BDDor cfg1 (node1' :: ul) node1' node2
  end.

Lemma BDDimpl_config_OK : BDDconfig_OK (fst BDDimpl).
Proof.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad BDDimpl) (@snd BDDconfig ad BDDimpl)) (bool_fun_impl (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  unfold BDDimpl in |- *.  elim (prod_sum _ _ (BDDneg cfg ul node1)).  intros cfg1 H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H.  clear H.  intros node1' H.  rewrite H.  apply BDDor_config_OK.
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).  apply BDDneg_config_OK.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).  apply BDDneg_list_OK_cons.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node_ul.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite H.  reflexivity.  assumption.  
Qed.

Lemma BDDimpl_node_OK : config_node_OK (fst BDDimpl) (snd BDDimpl).
Proof.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad BDDimpl) (@snd BDDconfig ad BDDimpl)) (bool_fun_impl (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  unfold BDDimpl in |- *.  elim (prod_sum _ _ (BDDneg cfg ul node1)).  intros cfg1 H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H.  clear H.  intros node1' H.  rewrite H.  apply BDDor_node_OK.
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).  apply BDDneg_config_OK.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).  apply BDDneg_list_OK_cons.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node_ul.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite H.  reflexivity.  assumption.  
Qed.

Lemma BDDimpl_used_nodes_preserved :
 used_nodes_preserved cfg (fst BDDimpl) ul.
Proof.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad BDDimpl) (@snd BDDconfig ad BDDimpl)) (bool_fun_impl (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  unfold BDDimpl in |- *.  elim (prod_sum _ _ (BDDneg cfg ul node1)).  intros cfg1 H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H.  clear H.  intros node1' H.  rewrite H.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_trans with (cfg2 := cfg1).  assumption.  
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  rewrite H.  reflexivity.  apply used_nodes_preserved_cons with (node := node1').
(* Goal: used_nodes_preserved cfg (@fst BDDconfig ad (BDDor cfg ul node1 node2)) ul *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
(* Goal: BDDconfig_OK cfg1 *)
  apply BDDor_used_nodes_preserved.
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).  apply BDDneg_config_OK.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).  apply BDDneg_list_OK_cons.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node_ul.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite H.  reflexivity.  assumption.  
Qed.

Lemma BDDimpl_is_impl :
 bool_fun_eq (bool_fun_of_BDD (fst BDDimpl) (snd BDDimpl))
   (bool_fun_impl (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)).
Proof.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad BDDimpl) (@snd BDDconfig ad BDDimpl)) (bool_fun_impl (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  unfold BDDimpl in |- *.  elim (prod_sum _ _ (BDDneg cfg ul node1)).  intros cfg1 H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H.  clear H.  intros node1' H.  rewrite H.
  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_or (bool_fun_of_BDD cfg1 node1')
                (bool_fun_of_BDD cfg1 node2)).
(* Goal: BDDconfig_OK cfg1 *)
  apply BDDor_is_or.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  rewrite H.
(* Goal: BDDconfig_OK cfg1 *)
  reflexivity.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).  apply BDDneg_list_OK_cons.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node_ul.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite H.  reflexivity.  assumption.  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_or (bool_fun_neg (bool_fun_of_BDD cfg node1))
                (bool_fun_of_BDD cfg node2)).
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply bool_fun_or_preserves_eq.  apply BDDneg_is_neg.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  apply used_nodes_preserved'_bool_fun with (ul := ul).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply BDDneg_config_OK.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  rewrite H.  reflexivity.  rewrite H.  reflexivity.
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply bool_fun_eq_sym.  apply bool_fun_impl_lemma.  
Qed.

Lemma BDDimpl_list_OK : used_list_OK (fst BDDimpl) ul.
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) ul *)
  apply used_nodes_preserved_list_OK with (cfg := cfg).  assumption.
(* Goal: used_nodes_preserved cfg (@fst BDDconfig ad BDDimpl) ul *)
  exact BDDimpl_used_nodes_preserved.
Qed.

Lemma BDDimpl_list_OK_cons : used_list_OK (fst BDDimpl) (snd BDDimpl :: ul).
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.  apply BDDimpl_node_OK.  exact BDDimpl_list_OK.  
Qed.


                         End BDDimpl_results.



                        Section BDDand_results.


Variable cfg : BDDconfig.
Variable ul : list ad.
Variable node1 node2 : ad.

Hypothesis cfg_OK : BDDconfig_OK cfg.
Hypothesis ul_OK : used_list_OK cfg ul.
Hypothesis used1 : used_node' cfg ul node1.
Hypothesis used2 : used_node' cfg ul node2.

Definition BDDand :=
  match BDDneg cfg ul node1 with
  | (cfg1, node1') =>
      match BDDneg cfg1 (node1' :: ul) node2 with
      | (cfg2, node2') =>
          match BDDor cfg2 (node2' :: node1' :: ul) node1' node2' with
          | (cfg3, node3) => BDDneg cfg3 (node3 :: ul) node3
          end
      end
  end.

Lemma BDDand_config_OK : BDDconfig_OK (fst BDDand).
Proof.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg1, node1') := BDDneg cfg ul node1 in let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg1, node1') := BDDneg cfg ul node1 in let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  unfold BDDand in |- *.  elim (prod_sum _ _ (BDDneg cfg ul node1)).  intros cfg1 H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H.  clear H.  intros node1' H.  rewrite H.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  elim (prod_sum _ _ (BDDneg cfg1 (node1' :: ul) node2)).  intros cfg2 H0.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H0.  clear H0.  intros node2' H0.  rewrite H0.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  elim (prod_sum _ _ (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2') (@pair BDDconfig ad x b))), @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  intros cfg3 H1.  elim H1.  clear H1.  intros node3 H1.  rewrite H1.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  cut (BDDconfig_OK cfg1).  cut (used_nodes_preserved cfg cfg1 ul).  intros.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg1 (node1' :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_node' cfg1 (node1' :: ul) node2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (BDDconfig_OK cfg2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_nodes_preserved cfg1 cfg2 (node1' :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg2 (node2' :: node1' :: ul)).  intro.
(* Goal: BDDconfig_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
  apply BDDneg_config_OK.
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_config_OK.  assumption.  assumption.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node'_ul.  apply used_node'_cons_node_ul.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  apply used_node'_cons_node_ul.  rewrite H1.  reflexivity.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
  replace node3 with
   (snd (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_node_OK.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H1.  reflexivity.  apply cons_OK_list_OK with (node := node1').
(* Goal: used_list_OK (@fst BDDconfig ad (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2')) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2')) cfg3 *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply cons_OK_list_OK with (node := node2').
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_list_OK.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node_ul.  
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) cfg2 *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node2' with (snd (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_list_OK_cons.  assumption.  assumption.  assumption.  rewrite H0.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H0.  reflexivity.  
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.  
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  rewrite H0.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).  apply BDDneg_list_OK_cons.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  rewrite H.
(* Goal: BDDconfig_OK cfg1 *)
  reflexivity.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  rewrite H.  reflexivity.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.
Qed.

Lemma BDDand_node_OK : config_node_OK (fst BDDand) (snd BDDand).
Proof.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg1, node1') := BDDneg cfg ul node1 in let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg1, node1') := BDDneg cfg ul node1 in let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  unfold BDDand in |- *.  elim (prod_sum _ _ (BDDneg cfg ul node1)).  intros cfg1 H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H.  clear H.  intros node1' H.  rewrite H.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  elim (prod_sum _ _ (BDDneg cfg1 (node1' :: ul) node2)).  intros cfg2 H0.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H0.  clear H0.  intros node2' H0.  rewrite H0.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  elim (prod_sum _ _ (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2') (@pair BDDconfig ad x b))), @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  intros cfg3 H1.  elim H1.  clear H1.  intros node3 H1.  rewrite H1.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  cut (BDDconfig_OK cfg1).  cut (used_nodes_preserved cfg cfg1 ul).  intros.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg1 (node1' :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_node' cfg1 (node1' :: ul) node2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (BDDconfig_OK cfg2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_nodes_preserved cfg1 cfg2 (node1' :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg2 (node2' :: node1' :: ul)).  intro.


(* Goal: config_node_OK (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply BDDneg_node_OK.


(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_config_OK.  assumption.  assumption.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node'_ul.  apply used_node'_cons_node_ul.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  apply used_node'_cons_node_ul.  rewrite H1.  reflexivity.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
  replace node3 with
   (snd (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_node_OK.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H1.  reflexivity.  apply cons_OK_list_OK with (node := node1').
(* Goal: used_list_OK (@fst BDDconfig ad (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2')) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2')) cfg3 *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply cons_OK_list_OK with (node := node2').
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_list_OK.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node_ul.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) cfg2 *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node2' with (snd (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_list_OK_cons.  assumption.  assumption.  assumption.  rewrite H0.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  rewrite H0.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).  apply BDDneg_list_OK_cons.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  rewrite H.
(* Goal: BDDconfig_OK cfg1 *)
  reflexivity.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  rewrite H.  reflexivity.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.

Qed.

Lemma BDDand_used_nodes_preserved : used_nodes_preserved cfg (fst BDDand) ul.
Proof.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg1, node1') := BDDneg cfg ul node1 in let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg1, node1') := BDDneg cfg ul node1 in let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  unfold BDDand in |- *.  elim (prod_sum _ _ (BDDneg cfg ul node1)).  intros cfg1 H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H.  clear H.  intros node1' H.  rewrite H.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  elim (prod_sum _ _ (BDDneg cfg1 (node1' :: ul) node2)).  intros cfg2 H0.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H0.  clear H0.  intros node2' H0.  rewrite H0.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  elim (prod_sum _ _ (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2') (@pair BDDconfig ad x b))), @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  intros cfg3 H1.  elim H1.  clear H1.  intros node3 H1.  rewrite H1.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  cut (BDDconfig_OK cfg1).  cut (used_nodes_preserved cfg cfg1 ul).  intros.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg1 (node1' :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_node' cfg1 (node1' :: ul) node2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (BDDconfig_OK cfg2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_nodes_preserved cfg1 cfg2 (node1' :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg2 (node2' :: node1' :: ul)).  intro.


(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_trans with (cfg2 := cfg3).  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_trans with (cfg2 := cfg1).  assumption.  assumption.
(* Goal: used_nodes_preserved cfg1 cfg3 ul *)
(* Goal: used_nodes_preserved cfg3 (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) ul *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_nodes_preserved_cons with (node := node1').
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_trans with (cfg2 := cfg2).  assumption.  assumption.
(* Goal: used_nodes_preserved cfg2 cfg3 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg3 (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) ul *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_nodes_preserved_cons with (node := node2').
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_used_nodes_preserved.  assumption.  assumption.  
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node'_ul.  apply used_node'_cons_node_ul.  
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  apply used_node'_cons_node_ul.  rewrite H1.  reflexivity.  
(* Goal: used_nodes_preserved cfg2 (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) ul *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_nodes_preserved_cons with (node := node3).
(* Goal: used_nodes_preserved cfg (@fst BDDconfig ad (BDDneg cfg ul node1)) ul *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: BDDconfig_OK cfg1 *)
  apply BDDneg_used_nodes_preserved.


(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_config_OK.  assumption.  assumption.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node'_ul.  apply used_node'_cons_node_ul.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  apply used_node'_cons_node_ul.  rewrite H1.  reflexivity.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
  replace node3 with
   (snd (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_node_OK.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H1.  reflexivity.  apply cons_OK_list_OK with (node := node1').
(* Goal: used_list_OK (@fst BDDconfig ad (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2')) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2')) cfg3 *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply cons_OK_list_OK with (node := node2').
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_list_OK.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node_ul.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) cfg2 *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node2' with (snd (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_list_OK_cons.  assumption.  assumption.  assumption.  rewrite H0.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  rewrite H0.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).  apply BDDneg_list_OK_cons.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  rewrite H.
(* Goal: BDDconfig_OK cfg1 *)
  reflexivity.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  rewrite H.  reflexivity.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.
Qed.

Lemma BDDand_is_and :
 bool_fun_eq (bool_fun_of_BDD (fst BDDand) (snd BDDand))
   (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)).
Proof.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg1, node1') := BDDneg cfg ul node1 in let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg1, node1') := BDDneg cfg ul node1 in let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  unfold BDDand in |- *.  elim (prod_sum _ _ (BDDneg cfg ul node1)).  intros cfg1 H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H.  clear H.  intros node1' H.  rewrite H.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  elim (prod_sum _ _ (BDDneg cfg1 (node1' :: ul) node2)).  intros cfg2 H0.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H0.  clear H0.  intros node2' H0.  rewrite H0.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  elim (prod_sum _ _ (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2') (@pair BDDconfig ad x b))), @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  intros cfg3 H1.  elim H1.  clear H1.  intros node3 H1.  rewrite H1.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  cut (BDDconfig_OK cfg1).  cut (used_nodes_preserved cfg cfg1 ul).  intros.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg1 (node1' :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_node' cfg1 (node1' :: ul) node2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (BDDconfig_OK cfg2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_nodes_preserved cfg1 cfg2 (node1' :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg2 (node2' :: node1' :: ul)).  intro.


  cut
   (bool_fun_eq
      (bool_fun_of_BDD (fst (BDDneg cfg3 (node3 :: ul) node3))
         (snd (BDDneg cfg3 (node3 :: ul) node3)))
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
      (bool_fun_neg (bool_fun_of_BDD cfg3 node3))).  intro.
  apply
   bool_fun_eq_trans with (bf2 := bool_fun_neg (bool_fun_of_BDD cfg3 node3)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_neg
                (bool_fun_or (bool_fun_of_BDD cfg2 node1')
                   (bool_fun_of_BDD cfg2 node2'))).
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply bool_fun_neg_preserves_eq.  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
  replace node3 with
   (snd (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_is_or.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H1.  reflexivity.  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_neg
                (bool_fun_or (bool_fun_neg (bool_fun_of_BDD cfg node1))
                   (bool_fun_neg (bool_fun_of_BDD cfg node2)))).
(* Goal: bool_fun_eq (bool_fun_or (bool_fun_of_BDD cfg2 node1') (bool_fun_of_BDD cfg2 node2')) (bool_fun_or (bool_fun_neg (bool_fun_of_BDD cfg node1)) (bool_fun_neg (bool_fun_of_BDD cfg node2))) *)
(* Goal: bool_fun_eq (bool_fun_neg (bool_fun_or (bool_fun_neg (bool_fun_of_BDD cfg node1)) (bool_fun_neg (bool_fun_of_BDD cfg node2)))) (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) (bool_fun_neg (bool_fun_of_BDD cfg3 node3)) *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply bool_fun_neg_preserves_eq.  apply bool_fun_or_preserves_eq.
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node1') (bool_fun_neg (bool_fun_of_BDD cfg node1)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node2') (bool_fun_neg (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_neg (bool_fun_or (bool_fun_neg (bool_fun_of_BDD cfg node1)) (bool_fun_neg (bool_fun_of_BDD cfg node2)))) (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) (bool_fun_neg (bool_fun_of_BDD cfg3 node3)) *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg1 node1').
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved'_bool_fun with (ul := node1' :: ul).  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  apply used_node'_cons_node_ul.
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).  apply BDDneg_is_neg.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply
   bool_fun_eq_trans with (bf2 := bool_fun_neg (bool_fun_of_BDD cfg1 node2)).
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) cfg2 *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node2' with (snd (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_is_neg.  assumption.  assumption.  assumption.  rewrite H0.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H0.  reflexivity.  apply bool_fun_neg_preserves_eq.
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved'_bool_fun with (ul := ul).  assumption.  rewrite H.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  rewrite H.  assumption.  assumption.  assumption.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply bool_fun_eq_sym.  apply bool_fun_and_lemma.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) (bool_fun_neg (bool_fun_of_BDD cfg3 node3)) *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply BDDneg_is_neg.


(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_config_OK.  assumption.  assumption.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node'_ul.  apply used_node'_cons_node_ul.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  apply used_node'_cons_node_ul.  rewrite H1.  reflexivity.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
  replace node3 with
   (snd (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_node_OK.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H1.  reflexivity.  apply cons_OK_list_OK with (node := node1').
(* Goal: used_list_OK (@fst BDDconfig ad (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2')) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2')) cfg3 *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply cons_OK_list_OK with (node := node2').
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_list_OK.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node_ul.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) cfg2 *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node2' with (snd (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_list_OK_cons.  assumption.  assumption.  assumption.  rewrite H0.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  rewrite H0.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).  apply BDDneg_list_OK_cons.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  rewrite H.
(* Goal: BDDconfig_OK cfg1 *)
  reflexivity.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  rewrite H.  reflexivity.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.
Qed.

Lemma BDDand_list_OK : used_list_OK (fst BDDand) ul.
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) ul *)
  apply used_nodes_preserved_list_OK with (cfg := cfg).  assumption.  
(* Goal: used_nodes_preserved cfg (@fst BDDconfig ad BDDand) ul *)
  exact BDDand_used_nodes_preserved.
Qed.

Lemma BDDand_list_OK_cons : used_list_OK (fst BDDand) (snd BDDand :: ul).
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.  apply BDDand_node_OK.  exact BDDand_list_OK.  
Qed.

Lemma BDDand_var_le :
 Nleb (node_height (fst BDDand) (snd BDDand))
   (BDDvar_max (node_height cfg node1) (node_height cfg node2)) = true.
Proof.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg1, node1') := BDDneg cfg ul node1 in let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg1, node1') := BDDneg cfg ul node1 in let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  unfold BDDand in |- *.  elim (prod_sum _ _ (BDDneg cfg ul node1)).  intros cfg1 H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H.  clear H.  intros node1' H.  rewrite H.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg2, node2') := BDDneg cfg1 (@cons ad node1' ul) node2 in let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  elim (prod_sum _ _ (BDDneg cfg1 (node1' :: ul) node2)).  intros cfg2 H0.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim H0.  clear H0.  intros node2' H0.  rewrite H0.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  elim (prod_sum _ _ (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2') (@pair BDDconfig ad x b))), @eq bool (Nleb (node_height (@fst BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (let (cfg3, node3) := BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2' in BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
  intros cfg3 H1.  elim H1.  clear H1.  intros node3 H1.  rewrite H1.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  cut (BDDconfig_OK cfg1).  cut (used_nodes_preserved cfg cfg1 ul).  intros.
(* Goal: @eq bool (Nleb (node_height (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg1 (node1' :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_node' cfg1 (node1' :: ul) node2).  intro.  cut (BDDconfig_OK cfg2).
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  intro.  cut (used_nodes_preserved cfg1 cfg2 (node1' :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg2 (node2' :: node1' :: ul)).  intro.
  replace
   (node_height (fst (BDDneg cfg3 (node3 :: ul) node3))
      (snd (BDDneg cfg3 (node3 :: ul) node3))) with 
   (node_height cfg3 node3).
(* Goal: @eq bool (Nleb (node_height cfg3 node3) (BDDvar_max (node_height cfg node1) (node_height cfg node2))) true *)
(* Goal: @eq N (node_height cfg3 node3) (node_height (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace (node_height cfg node1) with (node_height cfg2 node1').
(* Goal: @eq bool (Nleb (node_height cfg3 node3) (BDDvar_max (node_height cfg2 node1') (node_height cfg node2))) true *)
(* Goal: @eq N (node_height cfg2 node1') (node_height cfg node1) *)
(* Goal: @eq N (node_height cfg3 node3) (node_height (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace (node_height cfg node2) with (node_height cfg2 node2').
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
  replace node3 with
   (snd (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_var_le.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H1.  reflexivity.  
(* Goal: @eq N (node_height cfg2 node2') (node_height cfg node2) *)
(* Goal: @eq N (node_height cfg2 node1') (node_height cfg node1) *)
(* Goal: @eq N (node_height cfg3 node3) (node_height (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  transitivity (node_height cfg1 node2).
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) cfg2 *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node2' with (snd (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply Neqb_complete.  apply BDDneg_var_eq.  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  rewrite H0.  reflexivity.  rewrite H0.  reflexivity.  
(* Goal: BDDconfig_OK cfg1 *)
  apply Neqb_complete.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved'_node_height_eq with (ul := ul).  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  rewrite H.  reflexivity.  
(* Goal: @eq N (node_height (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) (node_height cfg3 node3) *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  transitivity (node_height cfg1 node1').  apply Neqb_complete.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: @eq bool (N.eqb (node_height (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) node1') (node_height cfg1 node1')) true *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) cfg2 *)
(* Goal: @eq N (node_height cfg1 node1') (node_height cfg node1) *)
(* Goal: @eq N (node_height cfg3 node3) (node_height (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_nodes_preserved'_node_height_eq with (ul := node1' :: ul).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply used_node'_cons_node_ul.  rewrite H0.  reflexivity.  
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).  apply Neqb_complete.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_var_eq.  assumption.  assumption.  assumption.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  reflexivity.  rewrite H.  reflexivity.  symmetry  in |- *.  apply Neqb_complete.
(* Goal: @eq bool (N.eqb (node_height (@fst BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3)) (@snd BDDconfig ad (BDDneg cfg3 (@cons ad node3 ul) node3))) (node_height cfg3 node3)) true *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply BDDneg_var_eq.
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_config_OK.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  reflexivity.  apply node_OK_list_OK.
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
  replace node3 with
   (snd (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_node_OK.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H1.  reflexivity.  
(* Goal: used_list_OK cfg3 ul *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg3 with (fst (BDDor cfg2 (node2' :: node1' :: ul) node1' node2')).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2')) ul *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg2 (@cons ad node2' (@cons ad node1' ul)) node1' node2')) cfg3 *)
(* Goal: used_node' cfg3 (@cons ad node3 ul) node3 *)
(* Goal: used_list_OK cfg2 (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply cons_OK_list_OK with (node := node1').  apply cons_OK_list_OK with (node := node2').
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_list_OK.  assumption.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  rewrite H1.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node_ul.  
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) (@cons ad node2' (@cons ad node1' ul)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg1 (@cons ad node1' ul) node2)) cfg2 *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node1' ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node2' with (snd (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_list_OK_cons.  assumption.  assumption.  assumption.  rewrite H0.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node1' ul) node2 *)
(* Goal: used_list_OK cfg1 (@cons ad node1' ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDneg cfg1 (node1' :: ul) node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  rewrite H0.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: used_list_OK (@fst BDDconfig ad (BDDneg cfg ul node1)) (@cons ad node1' ul) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDneg cfg ul node1)) cfg1 *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node1' with (snd (BDDneg cfg ul node1)).  apply BDDneg_list_OK_cons.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  rewrite H.  reflexivity.  rewrite H.
(* Goal: BDDconfig_OK cfg1 *)
  reflexivity.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  rewrite H.  reflexivity.  replace cfg1 with (fst (BDDneg cfg ul node1)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDneg_config_OK.  assumption.  assumption.  assumption.  rewrite H.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  reflexivity.
Qed.


                         End BDDand_results.



                       Section BDDiff_results.




Variable cfg : BDDconfig.
Variable ul : list ad.
Variable node1 node2 : ad.

Hypothesis cfg_OK : BDDconfig_OK cfg.
Hypothesis ul_OK : used_list_OK cfg ul.
Hypothesis used1 : used_node' cfg ul node1.
Hypothesis used2 : used_node' cfg ul node2.

Definition BDDiff :=
  match BDDor cfg ul node1 node2 with
  | (cfg1, node3) =>
      match BDDand cfg1 (node3 :: ul) node1 node2 with
      | (cfg2, node4) => BDDimpl cfg2 (node4 :: node3 :: ul) node3 node4
      end
  end.

Lemma BDDiff_config_OK : BDDconfig_OK (fst BDDiff).
Proof.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad BDDiff) (@snd BDDconfig ad BDDiff)) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  unfold BDDiff in |- *.  elim (prod_sum _ _ (BDDor cfg ul node1 node2)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDor cfg ul node1 node2) (@pair BDDconfig ad x b))), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  intros cfg1 H.  elim H.  clear H.  intros node3 H.  rewrite H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim (prod_sum _ _ (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDand cfg1 (@cons ad node3 ul) node1 node2) (@pair BDDconfig ad x b))), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  intros cfg2 H0.  elim H0.  clear H0.  intros node4 H0.  rewrite H0.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  cut (BDDconfig_OK cfg1).  intro.  cut (used_nodes_preserved cfg cfg1 ul).
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  intro.  cut (used_list_OK cfg1 (node3 :: ul)).  intro.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_node' cfg1 (node3 :: ul) node1).
(* Goal: forall (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (@None (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: bool_fun_eq (bool_fun_if x (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero)) (bool_fun_if x bool_fun_one bool_fun_zero) *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  cut (used_node' cfg1 (node3 :: ul) node2).  intros.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (BDDconfig_OK cfg2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_nodes_preserved cfg1 cfg2 (node3 :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg2 (node4 :: node3 :: ul)).  intro.
(* Goal: BDDconfig_OK (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply BDDimpl_config_OK.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_config_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite H0.  reflexivity.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: config_node_OK (@fst BDDconfig ad (BDDand cfg1 (@cons ad node3 ul) node1 node2)) node4 *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDand cfg1 (@cons ad node3 ul) node1 node2)) cfg2 *)
(* Goal: used_list_OK cfg2 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node4 with (snd (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_node_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.  rewrite H0.  reflexivity.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_list_OK with (cfg := cfg1).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  rewrite H0.  reflexivity.  
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_config_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply node_OK_list_OK.
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDor cfg ul node1 node2)).
(* Goal: config_node_OK (@fst BDDconfig ad (BDDor cfg ul node1 node2)) (@snd BDDconfig ad (BDDor cfg ul node1 node2)) *)
(* Goal: @eq ad (@snd BDDconfig ad (BDDor cfg ul node1 node2)) node3 *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
(* Goal: used_list_OK cfg1 ul *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node3 with (snd (BDDor cfg ul node1 node2)).  apply BDDor_node_OK.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  assumption.  rewrite H.  reflexivity.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) ul *)
  rewrite H.  reflexivity.  apply used_nodes_preserved_list_OK with (cfg := cfg).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  replace cfg1 with (fst (BDDor cfg ul node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_used_nodes_preserved.  assumption.  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  rewrite H.  reflexivity.
(* Goal: BDDconfig_OK (@fst BDDconfig ad (BDDor cfg ul node1 node2)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  replace cfg1 with (fst (BDDor cfg ul node1 node2)).  apply BDDor_config_OK.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  assumption.  rewrite H.  reflexivity.
Qed.

Lemma BDDiff_node_OK : config_node_OK (fst BDDiff) (snd BDDiff).
Proof.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad BDDiff) (@snd BDDconfig ad BDDiff)) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  unfold BDDiff in |- *.  elim (prod_sum _ _ (BDDor cfg ul node1 node2)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDor cfg ul node1 node2) (@pair BDDconfig ad x b))), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  intros cfg1 H.  elim H.  clear H.  intros node3 H.  rewrite H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim (prod_sum _ _ (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDand cfg1 (@cons ad node3 ul) node1 node2) (@pair BDDconfig ad x b))), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  intros cfg2 H0.  elim H0.  clear H0.  intros node4 H0.  rewrite H0.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  cut (BDDconfig_OK cfg1).  intro.  cut (used_nodes_preserved cfg cfg1 ul).
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  intro.  cut (used_list_OK cfg1 (node3 :: ul)).  intro.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_node' cfg1 (node3 :: ul) node1).
(* Goal: forall (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (@None (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: bool_fun_eq (bool_fun_if x (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero)) (bool_fun_if x bool_fun_one bool_fun_zero) *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  cut (used_node' cfg1 (node3 :: ul) node2).  intros.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (BDDconfig_OK cfg2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_nodes_preserved cfg1 cfg2 (node3 :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg2 (node4 :: node3 :: ul)).  intro.
(* Goal: config_node_OK (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply BDDimpl_node_OK.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_config_OK.  assumption.  assumption.  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite H0.  reflexivity.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.  
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: config_node_OK (@fst BDDconfig ad (BDDand cfg1 (@cons ad node3 ul) node1 node2)) node4 *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDand cfg1 (@cons ad node3 ul) node1 node2)) cfg2 *)
(* Goal: used_list_OK cfg2 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node4 with (snd (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_node_OK.  assumption.  assumption.  assumption.  assumption.  
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.  rewrite H0.  reflexivity.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_list_OK with (cfg := cfg1).  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  rewrite H0.  reflexivity.  
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_config_OK.  assumption.  assumption.  assumption.  assumption.  
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply node_OK_list_OK.
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDor cfg ul node1 node2)).
(* Goal: config_node_OK (@fst BDDconfig ad (BDDor cfg ul node1 node2)) (@snd BDDconfig ad (BDDor cfg ul node1 node2)) *)
(* Goal: @eq ad (@snd BDDconfig ad (BDDor cfg ul node1 node2)) node3 *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
(* Goal: used_list_OK cfg1 ul *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node3 with (snd (BDDor cfg ul node1 node2)).  apply BDDor_node_OK.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  assumption.  rewrite H.  reflexivity.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) ul *)
  rewrite H.  reflexivity.  apply used_nodes_preserved_list_OK with (cfg := cfg).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  replace cfg1 with (fst (BDDor cfg ul node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_used_nodes_preserved.  assumption.  assumption.  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  rewrite H.  reflexivity.
(* Goal: BDDconfig_OK (@fst BDDconfig ad (BDDor cfg ul node1 node2)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  replace cfg1 with (fst (BDDor cfg ul node1 node2)).  apply BDDor_config_OK.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  assumption.  rewrite H.  reflexivity.
Qed.

Lemma BDDiff_used_nodes_preserved : used_nodes_preserved cfg (fst BDDiff) ul.
Proof.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad BDDiff) (@snd BDDconfig ad BDDiff)) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  unfold BDDiff in |- *.  elim (prod_sum _ _ (BDDor cfg ul node1 node2)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDor cfg ul node1 node2) (@pair BDDconfig ad x b))), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  intros cfg1 H.  elim H.  clear H.  intros node3 H.  rewrite H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim (prod_sum _ _ (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDand cfg1 (@cons ad node3 ul) node1 node2) (@pair BDDconfig ad x b))), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  intros cfg2 H0.  elim H0.  clear H0.  intros node4 H0.  rewrite H0.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  cut (BDDconfig_OK cfg1).  intro.  cut (used_nodes_preserved cfg cfg1 ul).
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  intro.  cut (used_list_OK cfg1 (node3 :: ul)).  intro.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_node' cfg1 (node3 :: ul) node1).
(* Goal: forall (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (@None (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: bool_fun_eq (bool_fun_if x (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero)) (bool_fun_if x bool_fun_one bool_fun_zero) *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  cut (used_node' cfg1 (node3 :: ul) node2).  intros.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (BDDconfig_OK cfg2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_nodes_preserved cfg1 cfg2 (node3 :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg2 (node4 :: node3 :: ul)).  intro.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_trans with (cfg2 := cfg1).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_trans with (cfg2 := cfg2).  assumption.  
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_cons with (node := node3).  assumption.  
(* Goal: used_nodes_preserved cfg2 (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) ul *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_nodes_preserved_cons with (node := node3).
(* Goal: used_nodes_preserved cfg2 (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@cons ad node3 ul) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_nodes_preserved_cons with (node := node4).
(* Goal: used_nodes_preserved cfg2 (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply BDDimpl_used_nodes_preserved.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_config_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite H0.  reflexivity.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: config_node_OK (@fst BDDconfig ad (BDDand cfg1 (@cons ad node3 ul) node1 node2)) node4 *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDand cfg1 (@cons ad node3 ul) node1 node2)) cfg2 *)
(* Goal: used_list_OK cfg2 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node4 with (snd (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_node_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_list_OK with (cfg := cfg1).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_config_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply node_OK_list_OK.
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDor cfg ul node1 node2)).
(* Goal: config_node_OK (@fst BDDconfig ad (BDDor cfg ul node1 node2)) (@snd BDDconfig ad (BDDor cfg ul node1 node2)) *)
(* Goal: @eq ad (@snd BDDconfig ad (BDDor cfg ul node1 node2)) node3 *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
(* Goal: used_list_OK cfg1 ul *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node3 with (snd (BDDor cfg ul node1 node2)).  apply BDDor_node_OK.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  assumption.  rewrite H.  reflexivity.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) ul *)
  rewrite H.  reflexivity.  apply used_nodes_preserved_list_OK with (cfg := cfg).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  replace cfg1 with (fst (BDDor cfg ul node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  rewrite H.  reflexivity.
(* Goal: BDDconfig_OK (@fst BDDconfig ad (BDDor cfg ul node1 node2)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  replace cfg1 with (fst (BDDor cfg ul node1 node2)).  apply BDDor_config_OK.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  assumption.  rewrite H.  reflexivity.
Qed.

Lemma BDDiff_is_iff :
 bool_fun_eq (bool_fun_of_BDD (fst BDDiff) (snd BDDiff))
   (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)).
Proof.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad BDDiff) (@snd BDDconfig ad BDDiff)) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  unfold BDDiff in |- *.  elim (prod_sum _ _ (BDDor cfg ul node1 node2)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDor cfg ul node1 node2) (@pair BDDconfig ad x b))), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg1, node3) := BDDor cfg ul node1 node2 in let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  intros cfg1 H.  elim H.  clear H.  intros node3 H.  rewrite H.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  elim (prod_sum _ _ (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: forall (x : BDDconfig) (_ : @ex ad (fun b : ad => @eq (prod BDDconfig ad) (BDDand cfg1 (@cons ad node3 ul) node1 node2) (@pair BDDconfig ad x b))), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (let (cfg2, node4) := BDDand cfg1 (@cons ad node3 ul) node1 node2 in BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  intros cfg2 H0.  elim H0.  clear H0.  intros node4 H0.  rewrite H0.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
  cut (BDDconfig_OK cfg1).  intro.  cut (used_nodes_preserved cfg cfg1 ul).
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  intro.  cut (used_list_OK cfg1 (node3 :: ul)).  intro.
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_node' cfg1 (node3 :: ul) node1).
(* Goal: forall (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (@None (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: bool_fun_eq (bool_fun_if x (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero)) (bool_fun_if x bool_fun_one bool_fun_zero) *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  cut (used_node' cfg1 (node3 :: ul) node2).  intros.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (BDDconfig_OK cfg2).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_nodes_preserved cfg1 cfg2 (node3 :: ul)).  intro.
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  cut (used_list_OK cfg2 (node4 :: node3 :: ul)).  intro.
  cut
   (bool_fun_eq
      (bool_fun_of_BDD
         (fst (BDDimpl cfg2 (node4 :: node3 :: ul) node3 node4))
         (snd (BDDimpl cfg2 (node4 :: node3 :: ul) node3 node4)))
      (bool_fun_impl (bool_fun_of_BDD cfg2 node3)
(* Goal: forall _ : bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)), bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
         (bool_fun_of_BDD cfg2 node4))).  intro.
  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_impl (bool_fun_of_BDD cfg2 node3)
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
                (bool_fun_of_BDD cfg2 node4)).  assumption.
  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_impl
                (bool_fun_or (bool_fun_of_BDD cfg node1)
                   (bool_fun_of_BDD cfg node2))
                (bool_fun_and (bool_fun_of_BDD cfg node1)
                   (bool_fun_of_BDD cfg node2))).
(* Goal: bool_fun_eq (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) (bool_fun_impl (bool_fun_or (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2))) *)
(* Goal: bool_fun_eq (bool_fun_impl (bool_fun_or (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply bool_fun_impl_preserves_eq.
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node3) (bool_fun_or (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node4) (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_impl (bool_fun_or (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg1 node3).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved'_bool_fun with (ul := node3 :: ul).  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  apply used_node'_cons_node_ul.  
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDor cfg ul node1 node2)).
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDor cfg ul node1 node2)) (@snd BDDconfig ad (BDDor cfg ul node1 node2))) (bool_fun_or (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: @eq ad (@snd BDDconfig ad (BDDor cfg ul node1 node2)) node3 *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
(* Goal: bool_fun_eq (bool_fun_of_BDD cfg2 node4) (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_impl (bool_fun_or (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node3 with (snd (BDDor cfg ul node1 node2)).  apply BDDor_is_or.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  assumption.  rewrite H.  reflexivity.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  rewrite H.  reflexivity.  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_and (bool_fun_of_BDD cfg1 node1)
                (bool_fun_of_BDD cfg1 node2)).
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: config_node_OK (@fst BDDconfig ad (BDDand cfg1 (@cons ad node3 ul) node1 node2)) node4 *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDand cfg1 (@cons ad node3 ul) node1 node2)) cfg2 *)
(* Goal: used_list_OK cfg2 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node4 with (snd (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_is_and.  assumption.  assumption.  assumption.  assumption.  
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.  rewrite H0.  reflexivity.  
(* Goal: bool_fun_eq (bool_fun_and (bool_fun_of_BDD cfg1 node1) (bool_fun_of_BDD cfg1 node2)) (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_impl (bool_fun_or (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2))) (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply bool_fun_and_preserves_eq.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved'_bool_fun with (ul := ul).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved'_bool_fun with (ul := ul).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  apply bool_fun_eq_sym.
(* Goal: bool_fun_eq (bool_fun_iff (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) (bool_fun_impl (bool_fun_or (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)) (bool_fun_and (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2))) *)
(* Goal: bool_fun_eq (bool_fun_of_BDD (@fst BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4)) (@snd BDDconfig ad (BDDimpl cfg2 (@cons ad node4 (@cons ad node3 ul)) node3 node4))) (bool_fun_impl (bool_fun_of_BDD cfg2 node3) (bool_fun_of_BDD cfg2 node4)) *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply bool_fun_iff_lemma.  apply BDDimpl_is_impl.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_config_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite H0.  reflexivity.  assumption.  apply used_node'_cons_node'_ul.
(* Goal: used_node' cfg2 (@cons ad node4 (@cons ad node3 ul)) node4 *)
(* Goal: used_list_OK cfg2 (@cons ad node4 (@cons ad node3 ul)) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  apply used_node'_cons_node_ul.  apply used_node'_cons_node_ul.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: config_node_OK (@fst BDDconfig ad (BDDand cfg1 (@cons ad node3 ul) node1 node2)) node4 *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDand cfg1 (@cons ad node3 ul) node1 node2)) cfg2 *)
(* Goal: used_list_OK cfg2 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg1 cfg2 (@cons ad node3 ul) *)
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node4 with (snd (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_node_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_list_OK with (cfg := cfg1).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  rewrite H0.  reflexivity.
(* Goal: BDDconfig_OK cfg2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node2 *)
(* Goal: used_node' cfg1 (@cons ad node3 ul) node1 *)
(* Goal: used_list_OK cfg1 (@cons ad node3 ul) *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg2 with (fst (BDDand cfg1 (node3 :: ul) node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDand_config_OK.  assumption.  assumption.  assumption.  assumption.
(* Goal: @eq BDDconfig (@fst BDDconfig ad (@pair BDDconfig ad cfg1 node3)) cfg1 *)
  rewrite H0.  reflexivity.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply used_node'_cons_node'_ul.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply used_nodes_preserved_used_node' with (cfg := cfg).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply node_OK_list_OK.
(* Goal: BDDconfig_OK cfg1 *)
  replace cfg1 with (fst (BDDor cfg ul node1 node2)).
(* Goal: config_node_OK (@fst BDDconfig ad (BDDor cfg ul node1 node2)) (@snd BDDconfig ad (BDDor cfg ul node1 node2)) *)
(* Goal: @eq ad (@snd BDDconfig ad (BDDor cfg ul node1 node2)) node3 *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
(* Goal: used_list_OK cfg1 ul *)
(* Goal: used_nodes_preserved cfg cfg1 ul *)
(* Goal: BDDconfig_OK cfg1 *)
  replace node3 with (snd (BDDor cfg ul node1 node2)).  apply BDDor_node_OK.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  assumption.  rewrite H.  reflexivity.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) ul *)
  rewrite H.  reflexivity.  apply used_nodes_preserved_list_OK with (cfg := cfg).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  replace cfg1 with (fst (BDDor cfg ul node1 node2)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply BDDor_used_nodes_preserved.  assumption.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  rewrite H.  reflexivity.
(* Goal: BDDconfig_OK (@fst BDDconfig ad (BDDor cfg ul node1 node2)) *)
(* Goal: @eq BDDconfig (@fst BDDconfig ad (BDDor cfg ul node1 node2)) cfg1 *)
  replace cfg1 with (fst (BDDor cfg ul node1 node2)).  apply BDDor_config_OK.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.  assumption.  assumption.  rewrite H.  reflexivity.
Qed.

Lemma BDDiff_list_OK : used_list_OK (fst BDDiff) ul.
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) ul *)
  apply used_nodes_preserved_list_OK with (cfg := cfg).  assumption.
(* Goal: used_nodes_preserved cfg (@fst BDDconfig ad BDDiff) ul *)
  exact BDDiff_used_nodes_preserved.  
Qed.

Lemma BDDiff_list_OK_cons : used_list_OK (fst BDDiff) (snd BDDiff :: ul).
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.  apply BDDiff_node_OK.  exact BDDiff_list_OK.  
Qed.



                         End BDDiff_results.




                     Section BDDvar_make_results.


Variable cfg : BDDconfig.
Variable ul : list ad.
Variable x : BDDvar.

Hypothesis cfg_OK : BDDconfig_OK cfg.
Hypothesis ul_OK : used_list_OK cfg ul.

Definition BDDvar_make := BDDmake gc cfg x BDDzero BDDone ul.

Lemma BDDvar_make_config_OK : BDDconfig_OK (fst BDDvar_make).
Proof.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  unfold BDDvar_make in |- *.  apply BDDmake_keeps_config_OK.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply used'_zero.  apply used'_one.  unfold bs_of_cfg in |- *.
(* Goal: forall (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (@None (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: bool_fun_eq (bool_fun_if x (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero)) (bool_fun_if x bool_fun_one bool_fun_zero) *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite (config_OK_zero _ cfg_OK).  intros.  discriminate.  unfold bs_of_cfg in |- *.
(* Goal: forall (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (@None (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: bool_fun_eq (bool_fun_if x (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero)) (bool_fun_if x bool_fun_one bool_fun_zero) *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite (config_OK_one _ cfg_OK).  intros.  discriminate.
Qed.

Lemma BDDvar_make_node_OK :
 config_node_OK (fst BDDvar_make) (snd BDDvar_make).
Proof.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  unfold BDDvar_make in |- *.  apply BDDmake_node_OK.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply used'_zero.  apply used'_one.  unfold bs_of_cfg in |- *.
(* Goal: forall (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (@None (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: bool_fun_eq (bool_fun_if x (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero)) (bool_fun_if x bool_fun_one bool_fun_zero) *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite (config_OK_zero _ cfg_OK).  intros.  discriminate.  unfold bs_of_cfg in |- *.
(* Goal: forall (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (@None (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: bool_fun_eq (bool_fun_if x (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero)) (bool_fun_if x bool_fun_one bool_fun_zero) *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite (config_OK_one _ cfg_OK).  intros.  discriminate.
Qed.

Lemma BDDvar_make_used_nodes_preserved :
 used_nodes_preserved cfg (fst BDDvar_make) ul.
Proof.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  unfold BDDvar_make in |- *.  apply BDDmake_preserves_used_nodes.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  assumption.
Qed.

Lemma BDDvar_make_list_OK : used_list_OK (fst BDDvar_make) ul.
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) ul *)
  apply used_nodes_preserved_list_OK with (cfg := cfg).  assumption.
(* Goal: used_nodes_preserved cfg (@fst BDDconfig ad BDDvar_make) ul *)
  exact BDDvar_make_used_nodes_preserved.
Qed.

Lemma BDDvar_make_list_OK_cons :
 used_list_OK (fst BDDvar_make) (snd BDDvar_make :: ul).
Proof.
(* Goal: used_list_OK (@fst BDDconfig ad BDDvar_make) (@cons ad (@snd BDDconfig ad BDDvar_make) ul) *)
  apply node_OK_list_OK.  exact BDDvar_make_node_OK.  exact BDDvar_make_list_OK.
Qed.

Lemma BDDvar_make_is_var :
 bool_fun_eq (bool_fun_of_BDD (fst BDDvar_make) (snd BDDvar_make))
   (bool_fun_var x).
Proof.
  apply
   bool_fun_eq_trans with (bf2 := bool_fun_if x bool_fun_one bool_fun_zero).
  apply
   bool_fun_eq_trans
    with
      (bf2 := bool_fun_if x (bool_fun_of_BDD cfg BDDone)
                (bool_fun_of_BDD cfg BDDzero)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  unfold BDDvar_make in |- *.  apply BDDmake_bool_fun.  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  assumption.  apply used'_zero.  apply used'_one.  unfold bs_of_cfg in |- *.
(* Goal: forall (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (@None (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: bool_fun_eq (bool_fun_if x (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero)) (bool_fun_if x bool_fun_one bool_fun_zero) *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite (config_OK_zero _ cfg_OK).  intros.  discriminate.  unfold bs_of_cfg in |- *.
(* Goal: forall (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (@None (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: bool_fun_eq (bool_fun_if x (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero)) (bool_fun_if x bool_fun_one bool_fun_zero) *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  rewrite (config_OK_one _ cfg_OK).  intros.  discriminate.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply bool_fun_if_preserves_eq.  apply bool_fun_of_BDD_one.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: bool_fun_eq (bool_fun_if x bool_fun_one bool_fun_zero) (bool_fun_var x) *)
  apply bool_fun_of_BDD_zero.  assumption.  apply bool_fun_eq_sym.
(* Goal: bool_fun_eq (bool_fun_var x) (bool_fun_if x bool_fun_one bool_fun_zero) *)
  apply bool_fun_var_lemma.
Qed.


                          End BDDvar_make_results.



End BDDop.
