(* 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 Wf_nat.
Require Import EqNat.
Require Import Peano_dec.
Require Import Ensembles.
Require Import Finite_sets.
Require Import Finite_sets_facts.
Require Import Image.
Require Import List.
Require Import Compare.
 
Require Import misc.
Require Import bool_fun.
Require Import myMap.
Require Import config.
Require Import alloc.
Require Import make.
Require Import neg.
Require Import or.
Require Import univ.
Require Import op.
Require Import tauto.
Require Import quant.
Require Import gc.
Require Import mu.

Section New.

Variable N : nat.

Definition var_env'_dash (ve : var_env') (n : nat) :=
  if leb N n then ve (n - N) else false.

Definition var_env''_dash (ve : var_env'') :=
  var_env'_to_env'' N (2 * N) (var_env'_dash (var_env''_to_env' ve)).
 
Fixpoint be_dash (be : bool_expr) : bool_expr :=
  match be with
  | Zero => Zero
  | One => One
  | Var x => Var (N_of_nat (N + nat_of_N x))
  | Neg be' => Neg (be_dash be')
  | Or be1 be2 => Or (be_dash be1) (be_dash be2)
  | ANd be1 be2 => ANd (be_dash be1) (be_dash be2)
  | Impl be1 be2 => Impl (be_dash be1) (be_dash be2)
  | Iff be1 be2 => Iff (be_dash be1) (be_dash be2)
  end.
 
Fixpoint renamef (f : ad -> ad) (be : bool_expr) {struct be} : bool_expr :=
  match be with
  | Zero => Zero
  | One => One
  | Var x => Var (f x)
  | Neg be' => Neg (renamef f be')
  | Or be1 be2 => Or (renamef f be1) (renamef f be2)
  | ANd be1 be2 => ANd (renamef f be1) (renamef f be2)
  | Impl be1 be2 => Impl (renamef f be1) (renamef f be2)
  | Iff be1 be2 => Iff (renamef f be1) (renamef f be2)
  end.

Definition renfnat (n m : nat) := if leb n m then m else m + N.

Definition renfnad (n : nat) (x : ad) := N_of_nat (renfnat n (nat_of_N x)). 

Lemma dash_renf :
 forall be : bool_expr,
 be_ok (var_lu 0 N) be -> be_dash be = renamef (renfnad N) be.
Proof.
(* Goal: forall (be : bool_expr) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x be) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' be ve) (eval_be' be ve') *)
  simple induction be.  reflexivity.  reflexivity.  unfold renamef in |- *.  simpl in |- *.
(* Goal: forall (be : bool_expr) (_ : le O N), @eq bool_expr be (renamef (renfnad O) be) *)
(* Goal: forall (n : nat) (_ : forall (be : bool_expr) (_ : le n N), @eq bool_expr (replacel be (lx_1 n) (lx'_1 N n)) (renamef (renfnad n) be)) (be : bool_expr) (_ : le (S n) N), @eq bool_expr (replacel be (lx_1 (S n)) (lx'_1 N (S n))) (renamef (renfnad (S n)) be) *)
  unfold renfnad in |- *.  unfold renfnat in |- *.  intros.  elim (var_ok_inv _ _ H).
(* Goal: @eq bool_expr (Var (N.of_nat (Init.Nat.add N (N.to_nat b)))) (Var (N.of_nat (if Nat.leb N (N.to_nat b) then N.to_nat b else Init.Nat.add (N.to_nat b) N))) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, @eq bool_expr (be_dash b) (renamef (renfnad N) b)) (_ : be_ok (var_lu O N) (Neg b)), @eq bool_expr (be_dash (Neg b)) (renamef (renfnad N) (Neg b)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, @eq bool_expr (be_dash b) (renamef (renfnad N) b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, @eq bool_expr (be_dash b0) (renamef (renfnad N) b0)) (_ : be_ok (var_lu O N) (Or b b0)), @eq bool_expr (be_dash (Or b b0)) (renamef (renfnad N) (Or b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, @eq bool_expr (be_dash b) (renamef (renfnad N) b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, @eq bool_expr (be_dash b0) (renamef (renfnad N) b0)) (_ : be_ok (var_lu O N) (ANd b b0)), @eq bool_expr (be_dash (ANd b b0)) (renamef (renfnad N) (ANd b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, @eq bool_expr (be_dash b) (renamef (renfnad N) b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, @eq bool_expr (be_dash b0) (renamef (renfnad N) b0)) (_ : be_ok (var_lu O N) (Impl b b0)), @eq bool_expr (be_dash (Impl b b0)) (renamef (renfnad N) (Impl b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, @eq bool_expr (be_dash b) (renamef (renfnad N) b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, @eq bool_expr (be_dash b0) (renamef (renfnad N) b0)) (_ : be_ok (var_lu O N) (Iff b b0)), @eq bool_expr (be_dash (Iff b b0)) (renamef (renfnad N) (Iff b b0)) *)
  cut (var_lu 0 N b = true).  intro.  unfold var_lu in H0.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (andb_prop _ _ H0).  intros.
(* Goal: @eq bool_expr (Var (N.of_nat (Init.Nat.add N (N.to_nat b)))) (Var (N.of_nat (if Nat.leb N (N.to_nat b) then N.to_nat b else Init.Nat.add (N.to_nat b) N))) *)
(* Goal: @eq bool (var_lu O N b) true *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, @eq bool_expr (be_dash b) (renamef (renfnad N) b)) (_ : be_ok (var_lu O N) (Neg b)), @eq bool_expr (be_dash (Neg b)) (renamef (renfnad N) (Neg b)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, @eq bool_expr (be_dash b) (renamef (renfnad N) b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, @eq bool_expr (be_dash b0) (renamef (renfnad N) b0)) (_ : be_ok (var_lu O N) (Or b b0)), @eq bool_expr (be_dash (Or b b0)) (renamef (renfnad N) (Or b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, @eq bool_expr (be_dash b) (renamef (renfnad N) b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, @eq bool_expr (be_dash b0) (renamef (renfnad N) b0)) (_ : be_ok (var_lu O N) (ANd b b0)), @eq bool_expr (be_dash (ANd b b0)) (renamef (renfnad N) (ANd b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, @eq bool_expr (be_dash b) (renamef (renfnad N) b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, @eq bool_expr (be_dash b0) (renamef (renfnad N) b0)) (_ : be_ok (var_lu O N) (Impl b b0)), @eq bool_expr (be_dash (Impl b b0)) (renamef (renfnad N) (Impl b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, @eq bool_expr (be_dash b) (renamef (renfnad N) b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, @eq bool_expr (be_dash b0) (renamef (renfnad N) b0)) (_ : be_ok (var_lu O N) (Iff b b0)), @eq bool_expr (be_dash (Iff b b0)) (renamef (renfnad N) (Iff b b0)) *)
  replace (leb N (nat_of_N b)) with false.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (plus_comm N (nat_of_N b)).  reflexivity.  symmetry  in |- *.
(* Goal: @eq bool (Nat.leb (S n) n) false *)
(* Goal: forall _ : @eq bool (N.eqb (N.of_nat n) b) false, @eq bool_expr (Var (renfnad (S n) b)) (if N.eqb (N.of_nat n) b then Var (ap' N n) else Var (renfnad n b)) *)
(* Goal: forall _ : @eq bool (Nat.leb n (N.to_nat b)) false, @eq bool_expr (Var (renfnad (S n) b)) (if N.eqb (ap n) (N.of_nat (if Nat.leb n (N.to_nat b) then N.to_nat b else Init.Nat.add (N.to_nat b) N)) then Var (ap' N n) else Var (renfnad n b)) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Neg b)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Neg b))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Or b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Or b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (ANd b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (ANd b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Impl b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Impl b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Iff b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Iff b b0))) *)
  apply leb_correct_conv.  unfold lt in |- *.  apply leb_complete.  assumption.  
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply var_ok_inv.  assumption.  intros.  simpl in |- *.  rewrite H.  reflexivity.  
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply neg_ok_inv.  assumption.  intros.  simpl in |- *.  rewrite H.  rewrite H0.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  exact (proj2 (or_ok_inv _ _ _ H1)).  
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  exact (proj1 (or_ok_inv _ _ _ H1)).  intros.  simpl in |- *.  rewrite H.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite H0.  reflexivity.  exact (proj2 (and_ok_inv _ _ _ H1)).  
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  exact (proj1 (and_ok_inv _ _ _ H1)).  intros.  simpl in |- *.  rewrite H.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite H0.  reflexivity.  exact (proj2 (impl_ok_inv _ _ _ H1)).  
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  exact (proj1 (impl_ok_inv _ _ _ H1)).  intros.  simpl in |- *.  rewrite H.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite H0.  reflexivity.  exact (proj2 (iff_ok_inv _ _ _ H1)).  
(* Goal: be_ok (var_lu O N) b *)
  exact (proj1 (iff_ok_inv _ _ _ H1)).
Qed.

Lemma dash_be_ok :
 forall be : bool_expr,
 be_ok (var_lu 0 N) be -> be_ok (var_lu N (2 * N)) (be_dash be).
Proof.
(* Goal: forall (be : bool_expr) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x be) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' be ve) (eval_be' be ve') *)
  simple induction be.  intro.  apply zero_ok.  intro.  apply one_ok.  intros.  simpl in |- *.
(* Goal: be_ok (var_lu N (Init.Nat.add N (Init.Nat.add N O))) (Var (N.of_nat (Init.Nat.add N (N.to_nat b)))) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b)) (_ : be_ok (var_lu O N) (Neg b)), be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash (Neg b)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b0)) (_ : be_ok (var_lu O N) (Or b b0)), be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash (Or b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b0)) (_ : be_ok (var_lu O N) (ANd b b0)), be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash (ANd b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b0)) (_ : be_ok (var_lu O N) (Impl b b0)), be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash (Impl b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b0)) (_ : be_ok (var_lu O N) (Iff b b0)), be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash (Iff b b0)) *)
  apply var_ok.  inversion H.  unfold var_lu in H1.  elim (andb_prop _ _ H1).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  unfold var_lu in |- *.  apply andb_true_intro.  split.
(* Goal: @eq bool (ve (N.to_nat b)) (if Nat.leb N (N.to_nat (N.of_nat (Init.Nat.add N (N.to_nat b)))) then ve (Init.Nat.sub (N.to_nat (N.of_nat (Init.Nat.add N (N.to_nat b)))) N) else false) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Neg b) ve) (eval_be' (be_dash (Neg b)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Or b b0) ve) (eval_be' (be_dash (Or b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (ANd b b0) ve) (eval_be' (be_dash (ANd b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Impl b b0) ve) (eval_be' (be_dash (Impl b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Iff b b0) ve) (eval_be' (be_dash (Iff b b0)) (var_env'_dash ve)) *)
  rewrite (nat_of_N_of_nat (N + nat_of_N b)).  apply leb_correct.
(* Goal: @eq bool (ve (N.to_nat b)) (if Nat.leb N (N.to_nat (N.of_nat (Init.Nat.add N (N.to_nat b)))) then ve (Init.Nat.sub (N.to_nat (N.of_nat (Init.Nat.add N (N.to_nat b)))) N) else false) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Neg b) ve) (eval_be' (be_dash (Neg b)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Or b b0) ve) (eval_be' (be_dash (Or b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (ANd b b0) ve) (eval_be' (be_dash (ANd b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Impl b b0) ve) (eval_be' (be_dash (Impl b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Iff b b0) ve) (eval_be' (be_dash (Iff b b0)) (var_env'_dash ve)) *)
  apply le_plus_l.  rewrite (nat_of_N_of_nat (N + nat_of_N b)).
(* Goal: @eq bool (Nat.leb (S (Init.Nat.add N (N.to_nat b))) (Init.Nat.add N (Init.Nat.add N O))) true *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b)) (_ : be_ok (var_lu O N) (Neg b)), be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash (Neg b)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b0)) (_ : be_ok (var_lu O N) (Or b b0)), be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash (Or b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b0)) (_ : be_ok (var_lu O N) (ANd b b0)), be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash (ANd b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b0)) (_ : be_ok (var_lu O N) (Impl b b0)), be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash (Impl b b0)) *)
(* Goal: forall (b : bool_expr) (_ : forall _ : be_ok (var_lu O N) b, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b)) (b0 : bool_expr) (_ : forall _ : be_ok (var_lu O N) b0, be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash b0)) (_ : be_ok (var_lu O N) (Iff b b0)), be_ok (var_lu N (Init.Nat.mul (S (S O)) N)) (be_dash (Iff b b0)) *)
  replace (S (N + nat_of_N b)) with (S N + nat_of_N b).
(* Goal: @eq bool (Nat.leb (S n) N) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (plus_Snm_nSm N (nat_of_N b)).  apply leb_correct.
(* Goal: le (Init.Nat.add (S (Init.Nat.sub n N)) N) (Init.Nat.add N N) *)
(* Goal: @eq nat (Init.Nat.add (S (Init.Nat.sub n N)) N) (S (Init.Nat.add (Init.Nat.sub n N) N)) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub n N) N) n *)
(* Goal: forall _ : @eq bool (Nat.leb N n) false, @In BinNums.N (N.of_nat n) (lx' N) *)
(* Goal: @eq bool (eval_be' (ANd t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply plus_le_compat.  apply le_n.  rewrite <- (plus_n_O N).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_complete.  assumption.  simpl in |- *.  reflexivity.  simpl in |- *.  intros.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  inversion H0.  apply neg_ok.  apply H.  assumption.  simpl in |- *.  intros.
(* Goal: @eq bool (eval_be' (exl (ANd t (be_dash be)) (lx' N)) ve) true *)
  inversion H1.  apply or_ok; [ apply H; assumption | apply H0; assumption ].
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simpl in |- *.  intros.  inversion H1.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply and_ok; [ apply H; assumption | apply H0; assumption ].  simpl in |- *.  intros.
(* Goal: @eq bool (eval_be' (exl (ANd t (be_dash be)) (lx' N)) ve) true *)
  inversion H1.  apply impl_ok; [ apply H; assumption | apply H0; assumption ].
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simpl in |- *.  intros.  inversion H1.
(* Goal: be_ok (var_lu N (Init.Nat.add N (Init.Nat.add N O))) (Iff (be_dash b) (be_dash b0)) *)
  apply iff_ok; [ apply H; assumption | apply H0; assumption ].
Qed.

Lemma eval_dash_lemma1 :
 forall (be : bool_expr) (ve : var_env'),
 eval_be' be ve = eval_be' (be_dash be) (var_env'_dash ve).
Proof.
(* Goal: forall (be : bool_expr) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x be) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' be ve) (eval_be' be ve') *)
  simple induction be.  unfold eval_be' in |- *.  simpl in |- *.  unfold bool_fun_zero in |- *.  reflexivity.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold eval_be' in |- *.  simpl in |- *.  unfold bool_fun_one in |- *.  reflexivity.  simpl in |- *.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold eval_be' in |- *.  simpl in |- *.  unfold bool_fun_var in |- *.  unfold var_env'_dash in |- *.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_to_env in |- *.  intros.
(* Goal: @eq bool (ve (N.to_nat b)) (if Nat.leb N (N.to_nat (N.of_nat (Init.Nat.add N (N.to_nat b)))) then ve (Init.Nat.sub (N.to_nat (N.of_nat (Init.Nat.add N (N.to_nat b)))) N) else false) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Neg b) ve) (eval_be' (be_dash (Neg b)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Or b b0) ve) (eval_be' (be_dash (Or b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (ANd b b0) ve) (eval_be' (be_dash (ANd b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Impl b b0) ve) (eval_be' (be_dash (Impl b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Iff b b0) ve) (eval_be' (be_dash (Iff b b0)) (var_env'_dash ve)) *)
  rewrite (nat_of_N_of_nat (N + nat_of_N b)).
(* Goal: @eq bool (ve (N.to_nat b)) (if Nat.leb N (Init.Nat.add N (N.to_nat b)) then ve (Init.Nat.sub (Init.Nat.add N (N.to_nat b)) N) else false) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Neg b) ve) (eval_be' (be_dash (Neg b)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Or b b0) ve) (eval_be' (be_dash (Or b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (ANd b b0) ve) (eval_be' (be_dash (ANd b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Impl b b0) ve) (eval_be' (be_dash (Impl b b0)) (var_env'_dash ve)) *)
(* Goal: forall (b : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b ve) (eval_be' (be_dash b) (var_env'_dash ve))) (b0 : bool_expr) (_ : forall ve : var_env', @eq bool (eval_be' b0 ve) (eval_be' (be_dash b0) (var_env'_dash ve))) (ve : var_env'), @eq bool (eval_be' (Iff b b0) ve) (eval_be' (be_dash (Iff b b0)) (var_env'_dash ve)) *)
  elim (sumbool_of_bool (leb N (N + nat_of_N b))).  intro y.  rewrite y.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (minus_plus N (nat_of_N b)).  reflexivity.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  replace (leb N (N + nat_of_N b)) with true.  intro.  discriminate.  
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  symmetry  in |- *.  apply leb_correct.  apply le_plus_l.  intros.  simpl in |- *.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold eval_be' in |- *.  unfold eval_be' in H.  simpl in |- *.  unfold bool_fun_neg in |- *.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (H ve).  reflexivity.  unfold eval_be' in |- *.  simpl in |- *.  unfold bool_fun_or in |- *.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  rewrite (H ve).  rewrite (H0 ve).  reflexivity.  unfold eval_be' in |- *.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simpl in |- *.  unfold bool_fun_and in |- *.  intros.  rewrite (H ve).  rewrite (H0 ve).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  unfold eval_be' in |- *.  simpl in |- *.  unfold bool_fun_impl in |- *.  intros.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (H ve).  rewrite (H0 ve).  reflexivity.  unfold eval_be' in |- *.  simpl in |- *.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold bool_fun_iff in |- *.  intros.  rewrite (H ve).  rewrite (H0 ve).  reflexivity.
Qed.
 
Definition var_env_or (ve1 ve2 : var_env) (x : ad) := ve1 x || ve2 x.
Definition var_env'_or (ve1 ve2 : var_env') (x : nat) := ve1 x || ve2 x.
 
Lemma forall_lemma1 :
 forall (be : bool_expr) (ve : var_env) (a : ad),
 bool_fun_of_bool_expr (forall_ a be) ve = true ->
 bool_fun_of_bool_expr be ve = true.
Proof.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  rewrite (forall_OK a be ve) in H.  unfold bool_fun_forall in H.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold bool_fun_and in H.  elim (andb_prop _ _ H).  intros.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (ve a)).  intro y.  rewrite <- H0.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold bool_fun_restrict in |- *.  apply (bool_fun_of_be_ext be).  intros.
(* Goal: @eq bool (if N.eqb x a then true else ve (N.to_nat x)) (augment (fun x : BDDvar => ve (N.to_nat x)) a true x) *)
(* Goal: forall (n : nat) (_ : @eq bool (if N.eqb (N.of_nat n) a then true else ve n) true), not (@In BinNums.N (N.of_nat n) l) *)
(* Goal: no_dup_list ad l *)
(* Goal: @eq bool (bool_fun_restrict (bool_fun_of_bool_expr (univl be l)) a false (var_env'_to_env ve)) true *)
  unfold augment in |- *.  elim (sumbool_of_bool (Neqb a x)).  intro y0.  rewrite y0.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (Neqb_complete _ _ y0) in y.  assumption.  intro y0.  rewrite y0.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  intro y.  rewrite <- H1.  unfold bool_fun_restrict in |- *.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (bool_fun_of_be_ext be).  intros.  unfold augment in |- *.
(* Goal: @eq bool (ve (N.to_nat x)) (if N.eqb a x then false else ve (N.to_nat x)) *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) l) *)
(* Goal: no_dup_list ad l *)
  elim (sumbool_of_bool (Neqb a x)).  intro y0.  rewrite y0.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (Neqb_complete _ _ y0) in y.  assumption.  intro y0.  rewrite y0.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.
Qed.

Lemma renamef_ext :
 forall (be : bool_expr) (f g : ad -> ad),
 (forall x : ad, f x = g x) -> renamef f be = renamef g be.
Proof.
(* Goal: forall (be : bool_expr) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x be) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' be ve) (eval_be' be ve') *)
  simple induction be.  reflexivity.  reflexivity.  simpl in |- *.  intros.  rewrite (H b).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  intros.  simpl in |- *.  rewrite (H _ _ H0).  reflexivity.  intros.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simpl in |- *.  rewrite (H _ _ H1).  rewrite (H0 _ _ H1).  reflexivity.  intros.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simpl in |- *.  rewrite (H _ _ H1).  rewrite (H0 _ _ H1).  reflexivity.  intros.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simpl in |- *.  rewrite (H _ _ H1).  rewrite (H0 _ _ H1).  reflexivity.  intros.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simpl in |- *.  rewrite (H _ _ H1).  rewrite (H0 _ _ H1).  reflexivity.
Qed.

Lemma renamef_id : forall be : bool_expr, renamef (fun x => x) be = be.
Proof.
(* Goal: forall (be : bool_expr) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x be) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' be ve) (eval_be' be ve') *)
  simple induction be.  reflexivity.  reflexivity.  reflexivity.  intros.  simpl in |- *.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite H.  reflexivity.  intros.  simpl in |- *.  rewrite H.  rewrite H0.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  intros.  simpl in |- *.  rewrite H.  rewrite H0.  reflexivity.  intros.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simpl in |- *.  rewrite H.  rewrite H0.  reflexivity.  intros.  simpl in |- *.  rewrite H.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite H0.  reflexivity.
Qed.

Lemma renamefS :
 forall (be : bool_expr) (n : nat),
 n < N ->
 renamef (renfnad (S n)) be =
 subst (ap n) (Var (ap' N n)) (renamef (renfnad n) be).
Proof.
(* Goal: forall (be : bool_expr) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x be) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' be ve) (eval_be' be ve') *)
  simple induction be.  simpl in |- *.  reflexivity.  reflexivity.  intros.  simpl in |- *.
(* Goal: forall (be : bool_expr) (_ : le O N), @eq bool_expr be (renamef (fun x : ad => N.of_nat (renfnat O (N.to_nat x))) be) *)
(* Goal: forall (n : nat) (_ : forall (be : bool_expr) (_ : le n N), @eq bool_expr (replacel be (lx_1 n) (lx'_1 N n)) (renamef (renfnad n) be)) (be : bool_expr) (_ : le (S n) N), @eq bool_expr (replacel be (lx_1 (S n)) (lx'_1 N (S n))) (renamef (renfnad (S n)) be) *)
  unfold renfnad at 2 in |- *.  unfold renfnat in |- *.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (leb n (nat_of_N b))).  intro y.  rewrite y.
(* Goal: @eq bool_expr (Var (N.of_nat (N.to_nat b))) (Var b) *)
(* Goal: @eq bool true (Nat.leb (S n) (N.to_nat b)) *)
(* Goal: forall _ : @eq bool (Nat.leb n (N.to_nat b)) false, @eq bool_expr (Var (renfnad (S n) b)) (if N.eqb (ap n) (N.of_nat (if Nat.leb n (N.to_nat b) then N.to_nat b else Init.Nat.add (N.to_nat b) N)) then Var (ap' N n) else Var (renfnad n b)) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Neg b)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Neg b))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Or b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Or b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (ANd b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (ANd b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Impl b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Impl b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Iff b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Iff b b0))) *)
  rewrite (N_of_nat_of_N b).  unfold ap in |- *.
(* Goal: forall _ : @eq bool (Nat.leb N (N.to_nat x)) false, @eq bool (ve' (N.to_nat x)) (if Nat.leb N (N.to_nat x) then ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N)) else false) *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (Neqb (N_of_nat n) b)).  intro y0.  rewrite y0.
(* Goal: forall (be : bool_expr) (_ : le O N), @eq bool_expr be (renamef (fun x : ad => N.of_nat (renfnat O (N.to_nat x))) be) *)
(* Goal: forall (n : nat) (_ : forall (be : bool_expr) (_ : le n N), @eq bool_expr (replacel be (lx_1 n) (lx'_1 N n)) (renamef (renfnad n) be)) (be : bool_expr) (_ : le (S n) N), @eq bool_expr (replacel be (lx_1 (S n)) (lx'_1 N (S n))) (renamef (renfnad (S n)) be) *)
  unfold renfnad, ap' in |- *.  unfold renfnat in |- *.  rewrite <- (Neqb_complete _ _ y0).
(* Goal: @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (nat_of_N_of_nat n).  replace (leb (S n) n) with false.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (plus_comm n N).  reflexivity.  symmetry  in |- *.  apply leb_correct_conv.
(* Goal: forall (be : bool_expr) (_ : le O N), @eq bool_expr be (renamef (renfnad O) be) *)
(* Goal: forall (n : nat) (_ : forall (be : bool_expr) (_ : le n N), @eq bool_expr (replacel be (lx_1 n) (lx'_1 N n)) (renamef (renfnad n) be)) (be : bool_expr) (_ : le (S n) N), @eq bool_expr (replacel be (lx_1 (S n)) (lx'_1 N (S n))) (renamef (renfnad (S n)) be) *)
  auto.  intro y0.  rewrite y0.  unfold renfnad in |- *.  unfold renfnat in |- *.  rewrite y.
(* Goal: @eq bool_expr (Var (N.of_nat (N.to_nat b))) (Var b) *)
(* Goal: @eq bool true (Nat.leb (S n) (N.to_nat b)) *)
(* Goal: forall _ : @eq bool (Nat.leb n (N.to_nat b)) false, @eq bool_expr (Var (renfnad (S n) b)) (if N.eqb (ap n) (N.of_nat (if Nat.leb n (N.to_nat b) then N.to_nat b else Init.Nat.add (N.to_nat b) N)) then Var (ap' N n) else Var (renfnad n b)) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Neg b)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Neg b))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Or b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Or b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (ANd b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (ANd b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Impl b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Impl b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Iff b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Iff b b0))) *)
  rewrite (N_of_nat_of_N b).  replace (leb (S n) (nat_of_N b)) with true.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (N_of_nat_of_N b).  reflexivity.  symmetry  in |- *.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (le_le_S_eq _ _ (leb_complete _ _ y)).  intro.  apply leb_correct.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  assumption.  intro.  rewrite H0 in y0.  rewrite (N_of_nat_of_N b) in y0.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (Neqb_correct b) in y0.  discriminate.  intro y.  rewrite y.
(* Goal: @eq bool_expr (Var (renfnad (S n) b)) (if N.eqb (ap n) (N.of_nat (Init.Nat.add (N.to_nat b) N)) then Var (ap' N n) else Var (renfnad n b)) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Neg b)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Neg b))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Or b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Or b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (ANd b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (ANd b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Impl b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Impl b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Iff b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Iff b b0))) *)
  unfold renfnad at 1 in |- *.  unfold renfnat at 1 in |- *.
(* Goal: @eq bool_expr (Var (N.of_nat (if Nat.leb (S n) (N.to_nat b) then N.to_nat b else Init.Nat.add (N.to_nat b) N))) (if N.eqb (ap n) (N.of_nat (Init.Nat.add (N.to_nat b) N)) then Var (ap' N n) else Var (renfnad n b)) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Neg b)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Neg b))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Or b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Or b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (ANd b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (ANd b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Impl b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Impl b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Iff b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Iff b b0))) *)
  replace (leb (S n) (nat_of_N b)) with false.
(* Goal: @eq bool_expr (Var (N.of_nat (Init.Nat.add (N.to_nat b) N))) (if N.eqb (ap n) (N.of_nat (Init.Nat.add (N.to_nat b) N)) then Var (ap' N n) else Var (renfnad n b)) *)
(* Goal: @eq bool false (Nat.leb (S n) (N.to_nat b)) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Neg b)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Neg b))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Or b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Or b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (ANd b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (ANd b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Impl b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Impl b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Iff b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Iff b b0))) *)
  replace (Neqb (ap n) (N_of_nat (nat_of_N b + N))) with false.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold renfnad in |- *.  unfold renfnat in |- *.  rewrite y.  reflexivity.  symmetry  in |- *.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply not_true_is_false.  unfold not in |- *; intro.  unfold ap in H0.
(* Goal: False *)
(* Goal: @eq bool false (Nat.leb (S n) (N.to_nat b)) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Neg b)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Neg b))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Or b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Or b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (ANd b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (ANd b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Impl b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Impl b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Iff b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Iff b b0))) *)
  rewrite <- (nat_of_N_of_nat n) in H.
(* Goal: False *)
(* Goal: @eq bool false (Nat.leb (S n) (N.to_nat b)) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Neg b)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Neg b))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Or b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Or b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (ANd b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (ANd b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Impl b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Impl b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Iff b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Iff b b0))) *)
  rewrite (Neqb_complete _ _ H0) in H.
(* Goal: False *)
(* Goal: @eq bool false (Nat.leb (S n) (N.to_nat b)) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Neg b)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Neg b))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Or b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Or b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (ANd b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (ANd b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Impl b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Impl b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Iff b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Iff b b0))) *)
  rewrite (nat_of_N_of_nat (nat_of_N b + N)) in H.  apply (lt_irrefl N).
(* Goal: lt N N *)
(* Goal: @eq bool false (Nat.leb (S n) (N.to_nat b)) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Neg b)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Neg b))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Or b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Or b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (ANd b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (ANd b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Impl b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Impl b b0))) *)
(* Goal: forall (b : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b))) (b0 : bool_expr) (_ : forall (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) b0) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) b0))) (n : nat) (_ : lt n N), @eq bool_expr (renamef (renfnad (S n)) (Iff b b0)) (subst (ap n) (Var (ap' N n)) (renamef (renfnad n) (Iff b b0))) *)
  apply le_lt_trans with (m := nat_of_N b + N).  apply le_plus_r.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  assumption.  symmetry  in |- *.  apply not_true_is_false.  unfold not in |- *; intro.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  cut (leb n (nat_of_N b) = true).  intro.  rewrite H1 in y.  discriminate.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_correct.  apply le_trans with (m := S n).  apply le_S.  apply le_n.  apply leb_complete.  assumption.  intros.  simpl in |- *.  rewrite (H n H0).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  intros.  simpl in |- *.  rewrite (H n H1).  rewrite (H0 n H1).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  intros.  simpl in |- *.  rewrite (H n H1).  rewrite (H0 n H1).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  intros.  simpl in |- *.  rewrite (H n H1).  rewrite (H0 n H1).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  intros.  simpl in |- *.  rewrite (H n H1).  rewrite (H0 n H1).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.
Qed.

Lemma replacel_lemma :
 forall (n : nat) (be : bool_expr),
 n <= N -> replacel be (lx_1 n) (lx'_1 N n) = renamef (renfnad n) be.
Proof.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simple induction n.  simpl in |- *.  unfold renfnad in |- *.  unfold renfnat in |- *.  intro.  intro.
  replace
   (renamef
      (fun x : ad =>
       N_of_nat
         match leb 0 (nat_of_N x) with
         | true => nat_of_N x
         | false => nat_of_N x + N
         end) be) with (renamef (fun x => x) be).
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  symmetry  in |- *.  apply renamef_id.  apply renamef_ext.  intro.
(* Goal: @eq ad x (N.of_nat (if Nat.leb O (N.to_nat x) then N.to_nat x else Init.Nat.add (N.to_nat x) N)) *)
(* Goal: forall (n : nat) (_ : forall (be : bool_expr) (_ : le n N), @eq bool_expr (replacel be (lx_1 n) (lx'_1 N n)) (renamef (renfnad n) be)) (be : bool_expr) (_ : le (S n) N), @eq bool_expr (replacel be (lx_1 (S n)) (lx'_1 N (S n))) (renamef (renfnad (S n)) be) *)
  rewrite (leb_correct 0 (nat_of_N x) (le_O_n _)).  symmetry  in |- *.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply N_of_nat_of_N.  simpl in |- *.  intros.  rewrite (H be).  unfold replace in |- *.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  symmetry  in |- *.  unfold replace in |- *.  apply renamefS.  assumption.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply le_trans with (m := S n0).  apply le_S.  apply le_n.  assumption.
Qed.

Lemma replacel_lemma2 :
 forall be : bool_expr,
 be_ok (var_lu 0 N) be -> replacel be (lx N) (lx' N) = be_dash be.
Proof.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  unfold lx, lx' in |- *.  rewrite (replacel_lemma N be (le_n _)).  symmetry  in |- *.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply dash_renf.  assumption.
Qed.

Lemma exl_semantics :
 forall (lx : list ad) (be : bool_expr) (ve : var_env'),
 (forall n : nat, ve n = true -> ~ In (N_of_nat n) lx) ->
 no_dup_list _ lx ->
 (eval_be' (exl be lx) ve = true <->
  (exists ve' : var_env',
     (forall n : nat, ve' n = true -> In (N_of_nat n) lx) /\
     eval_be' be (var_env'_or ve ve') = true)).
Proof.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simple induction lx.  simpl in |- *.  intros be ve H H00.  split.  intro.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  split with (fun n : nat => false).  split.  intros.  discriminate.  unfold var_env'_or in |- *.
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve ve')) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- H0.  unfold eval_be' in |- *.  apply (bool_fun_of_be_ext be).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_to_env in |- *.  intro.  elim (ve (nat_of_N x)); reflexivity.  
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  elim H0; clear H0.  intros ve' H0.  inversion H0.  clear H0.
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve ve')) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- H2.  unfold eval_be' in |- *.  apply (bool_fun_of_be_ext be).
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_to_env in |- *.  unfold var_env'_or in |- *.  intro.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  replace (ve' (nat_of_N x)) with false.  elim (ve (nat_of_N x)); reflexivity.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  symmetry  in |- *.  apply not_true_is_false.  unfold not in |- *; intro.  exact (H1 _ H0).  
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros a l H be ve H0 H00.  split.  intros.  simpl in H1.
(* Goal: @eq bool (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve'))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold eval_be' in H1.
(* Goal: @ex var_env' (fun ve' : var_env' => and (forall (n : nat) (_ : @eq bool (ve' n) true), @In BinNums.N (N.of_nat n) (@cons ad a l)) (@eq bool (eval_be' be (var_env'_or ve ve')) true)) *)
(* Goal: forall _ : @ex var_env' (fun ve' : var_env' => and (forall (n : nat) (_ : @eq bool (ve' n) true), @In BinNums.N (N.of_nat n) (@cons ad a l)) (@eq bool (eval_be' be (var_env'_or ve ve')) true)), @eq bool (eval_be' (exl be (@cons ad a l)) ve) true *)
  rewrite (ex_OK a (exl be l) (var_env'_to_env ve)) in H1.
(* Goal: @ex var_env' (fun ve' : var_env' => and (forall (n : nat) (_ : @eq bool (ve' n) true), @In BinNums.N (N.of_nat n) (@cons ad a l)) (@eq bool (eval_be' be (var_env'_or ve ve')) true)) *)
(* Goal: forall _ : @ex var_env' (fun ve' : var_env' => and (forall (n : nat) (_ : @eq bool (ve' n) true), @In BinNums.N (N.of_nat n) (@cons ad a l)) (@eq bool (eval_be' be (var_env'_or ve ve')) true)), @eq bool (eval_be' (exl be (@cons ad a l)) ve) true *)
  unfold bool_fun_ex in H1.  unfold bool_fun_or in H1.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold bool_fun_restrict in H1.  elim (orb_prop _ _ H1); clear H1; intros.
  elim
   (H be
      (fun n : nat =>
       match Neqb (N_of_nat n) a with
       | true => true
       | false => ve n
       end)).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  clear H3.  elim H2.  intros ve' H3.  inversion H3.  clear H3.
  split
   with
     (fun n : nat =>
      match Neqb (N_of_nat n) a with
      | true => true
      | false => ve' n
      end).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  split.  intros.  elim (sumbool_of_bool (Neqb (N_of_nat n) a)).  intro y.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- (Neqb_complete _ _ y).  left.  reflexivity.  intro y.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite y in H3.  right.  apply H4; assumption.  
  replace
   (eval_be' be
      (var_env'_or ve
         (fun n : nat =>
          match Neqb (N_of_nat n) a with
          | true => true
          | false => ve' n
          end))) with
   (eval_be' be
      (var_env'_or
         (fun n : nat =>
          match Neqb (N_of_nat n) a with
          | true => true
          | false => ve n
          end) ve')).
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  assumption.  unfold eval_be', var_env'_or in |- *.  apply (bool_fun_of_be_ext be).
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_to_env in |- *.  intro.  rewrite (N_of_nat_of_N x).
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve ve')) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (Neqb x a).  auto with bool.  auto with bool.  unfold eval_be' in |- *.
  replace
   (bool_fun_of_bool_expr (exl be l)
      (var_env'_to_env
         (fun n : nat =>
          match Neqb (N_of_nat n) a with
          | true => true
          | false => ve n
          end))) with
   (bool_fun_of_bool_expr (exl be l) (augment (var_env'_to_env ve) a true)).
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  assumption.  apply (bool_fun_of_be_ext (exl be l)).
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold augment, var_env'_to_env in |- *.  intro.  rewrite (N_of_nat_of_N x).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (Neqb_comm a x).  reflexivity.  intros.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (Neqb (N_of_nat n) a)).  intro y.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (Neqb_complete _ _ y).  apply no_dup_cons_no_in.  assumption.  intro y.
(* Goal: not (@In BinNums.N (N.of_nat n) l) *)
(* Goal: no_dup_list ad l *)
(* Goal: @eq bool (bool_fun_restrict (bool_fun_of_bool_expr (univl be l)) a false (var_env'_to_env ve)) true *)
  rewrite y in H2.  simpl in H0.  exact (fun x => H0 _ H2 (or_intror _ x)).  
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply no_dup_cons_no_dup with (a := a).  assumption.  
  elim
   (H be
      (fun n : nat =>
       match Neqb (N_of_nat n) a with
       | true => false
       | false => ve n
       end)).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  clear H3 H.  elim H2.  intros ve' H.  inversion H.  clear H.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  clear H2.  split with ve'.  split.  intros.  right.  apply H3.  assumption.
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve ve')) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- H4.  unfold eval_be' in |- *.  apply (bool_fun_of_be_ext be).
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_to_env, var_env'_or in |- *.  intro.  rewrite (N_of_nat_of_N x).
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (Neqb x a)).  intro y.  rewrite y.  simpl in |- *.
(* Goal: no_dup_list BinNums.N (@cons BinNums.N (N.of_nat n) l) *)
(* Goal: forall _ : @eq bool (N.eqb (N.of_nat n) a) false, not (@In BinNums.N (N.of_nat n) l) *)
(* Goal: no_dup_list ad l *)
(* Goal: @eq bool (bool_fun_restrict (bool_fun_of_bool_expr (univl be l)) a false (var_env'_to_env ve)) true *)
  rewrite (Neqb_complete _ _ y).  elim (sumbool_of_bool (ve (nat_of_N a))).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  intro y0.  elim (H0 _ y0).  rewrite (N_of_nat_of_N a).  left.  reflexivity.  
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  intro y0.  rewrite y0.  reflexivity.  intro y.  rewrite y.  reflexivity.  
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve ve')) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- H1.  unfold eval_be' in |- *.  apply (bool_fun_of_be_ext (exl be l)).
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_to_env, augment in |- *.  intro.  rewrite (N_of_nat_of_N x).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (Neqb_comm a x).  reflexivity.  intros.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (Neqb (N_of_nat n) a)).  intro y.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (Neqb_complete _ _ y).  apply no_dup_cons_no_in.  assumption.  intro y.
(* Goal: not (@In BinNums.N (N.of_nat n) l) *)
(* Goal: no_dup_list ad l *)
(* Goal: @eq bool (bool_fun_restrict (bool_fun_of_bool_expr (univl be l)) a false (var_env'_to_env ve)) true *)
  rewrite y in H2.  exact (fun x => H0 _ H2 (or_intror _ x)).  
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply no_dup_cons_no_dup with (a := a).  assumption.  intros.  elim H1; clear H1.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  intros ve' H1.  inversion H1.  clear H1.  simpl in |- *.  unfold eval_be' in |- *.
(* Goal: @eq bool (bool_fun_of_bool_expr (be_ex a (exl be l)) (var_env'_to_env ve)) true *)
  rewrite (ex_OK a (exl be l) (var_env'_to_env ve)).  unfold bool_fun_ex in |- *.
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (bool_fun_of_bool_expr b (var_env'_to_env ve)) (bool_fun_of_bool_expr b (var_env'_to_env ve'))) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (bool_fun_of_bool_expr b0 (var_env'_to_env ve)) (bool_fun_of_bool_expr b0 (var_env'_to_env ve'))) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (orb (be_x_free x b) (be_x_free x b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (bool_fun_or (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0) (var_env'_to_env ve)) (bool_fun_or (bool_fun_of_bool_expr b) (bool_fun_of_bool_expr b0) (var_env'_to_env ve')) *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b0 ve) (eval_be' b0 ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (ANd b b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (ANd b b0) ve) (eval_be' (ANd b b0) ve') *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b0 ve) (eval_be' b0 ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (Impl b b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (Impl b b0) ve) (eval_be' (Impl b b0) ve') *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b0 ve) (eval_be' b0 ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (Iff b b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (Iff b b0) ve) (eval_be' (Iff b b0) ve') *)
  unfold bool_fun_or in |- *.  unfold bool_fun_restrict in |- *.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (ve' (nat_of_N a))).  intro y.
  elim
   (H be
      (fun n : nat =>
       match Neqb (N_of_nat n) a with
       | true => true
       | false => ve n
       end)).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  clear H1 H.  apply orb_true_intro.  left.
  replace
   (bool_fun_of_bool_expr (exl be l) (augment (var_env'_to_env ve) a true))
   with
   (eval_be' (exl be l)
      (fun n : nat =>
       match Neqb (N_of_nat n) a with
       | true => true
       | false => ve n
       end)).
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply H4.  split
   with
     (fun n : nat =>
      match Neqb (N_of_nat n) a with
      | true => false
      | false => ve' n
      end).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  split.  intros.  elim (sumbool_of_bool (Neqb (N_of_nat n) a)).  intro y0.
(* Goal: @In BinNums.N (N.of_nat n) (lx' N) *)
(* Goal: @eq bool (eval_be' (ANd t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite y0 in H.  discriminate.  intro y0.  rewrite y0 in H.  elim (H2 _ H).
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intro.  rewrite <- H1 in y0.  rewrite (Neqb_correct a) in y0.  discriminate.
(* Goal: or (@eq BinNums.N a (N.of_nat n)) (@In BinNums.N (N.of_nat n) l) *)
(* Goal: @eq bool (eval_be' (univl be l) ve) (bool_fun_of_bool_expr (univl be l) (augment (var_env'_to_env ve) a false)) *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) l) *)
(* Goal: no_dup_list ad l *)
  auto.  replace
   (eval_be' be
      (var_env'_or
         (fun n : nat =>
          match Neqb (N_of_nat n) a with
          | true => true
          | false => ve n
          end)
         (fun n : nat =>
          match Neqb (N_of_nat n) a with
          | true => false
          | false => ve' n
          end))) with (eval_be' be (var_env'_or ve ve')).
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  assumption.  unfold eval_be' in |- *.  apply (bool_fun_of_be_ext be).  intro x.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat (N.to_nat x)))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat (N.to_nat x)))) N) true), False *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_to_env, var_env'_or in |- *.  rewrite (N_of_nat_of_N x).
(* Goal: forall _ : @eq bool (Nat.leb N (N.to_nat x)) false, @eq bool (ve' (N.to_nat x)) (if Nat.leb N (N.to_nat x) then ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N)) else false) *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (Neqb x a)).  intro y0.  rewrite y0.
(* Goal: @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (Neqb_complete _ _ y0).  rewrite y.  auto with bool.  intro y0.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite y0.  reflexivity.  unfold eval_be' in |- *.
(* Goal: @eq bool (bool_fun_of_bool_expr (exl be l) (augment (var_env'_to_env ve) a false)) (bool_fun_of_bool_expr (exl be l) (var_env'_to_env ve)) *)
(* Goal: @ex var_env' (fun ve' : var_env' => and (forall (n : nat) (_ : @eq bool (ve' n) true), @In BinNums.N (N.of_nat n) l) (@eq bool (eval_be' be (var_env'_or ve ve')) true)) *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) l) *)
(* Goal: no_dup_list ad l *)
  apply (bool_fun_of_be_ext (exl be l)).  unfold var_env'_to_env, augment in |- *.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  rewrite (N_of_nat_of_N x).  rewrite (Neqb_comm a x).  reflexivity.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  elim (sumbool_of_bool (Neqb (N_of_nat n) a)).  intro y0.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (Neqb_complete _ _ y0).  apply no_dup_cons_no_in.  assumption.
(* Goal: forall _ : @eq bool (Nat.leb N (N.to_nat x)) false, @eq bool (ve' (N.to_nat x)) (if Nat.leb N (N.to_nat x) then ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N)) else false) *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  intro y0.  rewrite y0 in H1.  exact (fun x => H0 _ H1 (or_intror _ x)).  
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply no_dup_cons_no_dup with (a := a).  assumption.  intro y.  elim (H be ve).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  clear H H1.  apply orb_true_intro.  right.  rewrite <- H4.
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve ve')) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold eval_be' in |- *.  apply (bool_fun_of_be_ext (exl be l)).
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold augment, var_env'_to_env in |- *.  intro.  elim (sumbool_of_bool (Neqb a x)).
(* Goal: forall _ : @eq bool (Nat.leb N (N.to_nat x)) false, @eq bool (ve' (N.to_nat x)) (if Nat.leb N (N.to_nat x) then ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N)) else false) *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  intro y0.  rewrite y0.  symmetry  in |- *.  rewrite <- (Neqb_complete _ _ y0).
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply not_true_is_false.  unfold not in |- *; intro.  apply (H0 _ H).  left.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  symmetry  in |- *.  apply N_of_nat_of_N.  intro y0.  rewrite y0.  reflexivity.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  split with ve'.  split.  intros.  elim (H2 _ H).  intro.  rewrite H1 in y.
(* Goal: @In BinNums.N (N.of_nat n) (lx' N) *)
(* Goal: @eq bool (eval_be' (ANd t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (nat_of_N_of_nat n) in y.  rewrite H in y.  discriminate.  auto.  
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  assumption.  intros.  exact (fun x => H0 _ H1 (or_intror _ x)).  
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply no_dup_cons_no_dup with (a := a).  assumption.  
Qed.

Lemma univl_semantics :
 forall (lx : list ad) (be : bool_expr) (ve : var_env'),
 (forall n : nat, ve n = true -> ~ In (N_of_nat n) lx) ->
 no_dup_list _ lx ->
 (eval_be' (univl be lx) ve = true <->
  (forall ve' : var_env',
   (forall n : nat, ve' n = true -> In (N_of_nat n) lx) ->
   eval_be' be (var_env'_or ve ve') = true)).
Proof.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simple induction lx.  simpl in |- *.  intros be ve H H00.  intros.  split.  intro.  intros.
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve ve')) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold eval_be' in |- *.
  replace (bool_fun_of_bool_expr be (var_env'_to_env (var_env'_or ve ve')))
   with (bool_fun_of_bool_expr be (var_env'_to_env ve)).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  assumption.  apply (bool_fun_of_be_ext be).  intros.  unfold var_env'_or in |- *.
(* Goal: @eq bool (var_env'_to_env ve b) (var_env'_to_env ve' b) *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (Neg b)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (Neg b) ve) (eval_be' (Neg b) ve') *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b0 ve) (eval_be' b0 ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (Or b b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (Or b b0) ve) (eval_be' (Or b b0) ve') *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b0 ve) (eval_be' b0 ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (ANd b b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (ANd b b0) ve) (eval_be' (ANd b b0) ve') *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b0 ve) (eval_be' b0 ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (Impl b b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (Impl b b0) ve) (eval_be' (Impl b b0) ve') *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b0 ve) (eval_be' b0 ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (Iff b b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (Iff b b0) ve) (eval_be' (Iff b b0) ve') *)
  unfold var_env'_to_env in |- *.  replace (ve' (nat_of_N x)) with false.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (ve (nat_of_N x)); reflexivity.  symmetry  in |- *.  apply not_true_is_false.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold not in |- *; intro.  exact (H1 _ H2).  intros.
  replace (eval_be' be ve) with
   (eval_be' be (var_env'_or ve (fun n => false))).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply H0.  intros.  discriminate.  unfold eval_be' in |- *.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (bool_fun_of_be_ext be).  intro.  unfold var_env'_to_env in |- *.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_or in |- *.  elim (ve (nat_of_N x)); reflexivity.  simpl in |- *.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros a l H be ve H0 H00.  intros.  split.  intros.  unfold eval_be' in H1.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (ve' (nat_of_N a))).  intro y.
(* Goal: @eq bool (eval_be' be (var_env'_or ve ve')) true *)
(* Goal: forall _ : @eq bool (ve' (N.to_nat a)) false, @eq bool (eval_be' be (var_env'_or ve ve')) true *)
(* Goal: forall _ : forall (ve' : var_env') (_ : forall (n : nat) (_ : @eq bool (ve' n) true), or (@eq BinNums.N a (N.of_nat n)) (@In BinNums.N (N.of_nat n) l)), @eq bool (eval_be' be (var_env'_or ve ve')) true, @eq bool (eval_be' (forall_ a (univl be l)) ve) true *)
  rewrite (forall_OK a (univl be l) (var_env'_to_env ve)) in H1.
(* Goal: @eq bool (eval_be' be (var_env'_or ve ve')) true *)
(* Goal: forall _ : @eq bool (ve' (N.to_nat a)) false, @eq bool (eval_be' be (var_env'_or ve ve')) true *)
(* Goal: forall _ : forall (ve' : var_env') (_ : forall (n : nat) (_ : @eq bool (ve' n) true), or (@eq BinNums.N a (N.of_nat n)) (@In BinNums.N (N.of_nat n) l)), @eq bool (eval_be' be (var_env'_or ve ve')) true, @eq bool (eval_be' (forall_ a (univl be l)) ve) true *)
  unfold bool_fun_forall in H1.  unfold bool_fun_and in H1.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (andb_prop _ _ H1).  intros.  clear H1.  clear H4.
(* Goal: @eq bool (eval_be' be (var_env'_or ve ve')) true *)
(* Goal: forall _ : @eq bool (ve' (N.to_nat a)) false, @eq bool (eval_be' be (var_env'_or ve ve')) true *)
(* Goal: forall _ : forall (ve' : var_env') (_ : forall (n : nat) (_ : @eq bool (ve' n) true), or (@eq BinNums.N a (N.of_nat n)) (@In BinNums.N (N.of_nat n) l)), @eq bool (eval_be' be (var_env'_or ve ve')) true, @eq bool (eval_be' (forall_ a (univl be l)) ve) true *)
  unfold bool_fun_restrict in H3.
  replace (eval_be' be (var_env'_or ve ve')) with
   (eval_be' be
      (var_env'_or
         (fun n : nat =>
          match Neqb (N_of_nat n) a with
          | true => true
          | false => ve n
          end)
         (fun n : nat =>
          match Neqb (N_of_nat n) a with
          | true => false
          | false => ve' n
          end))).
  elim
   (H be
      (fun n : nat =>
       match Neqb (N_of_nat n) a with
       | true => true
       | false => ve n
       end)).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  clear H4.  apply H1.  unfold augment in H3.  unfold eval_be' in |- *.
  replace
   (bool_fun_of_bool_expr (univl be l)
      (var_env'_to_env
         (fun n : nat =>
          match Neqb (N_of_nat n) a with
          | true => true
          | false => ve n
          end))) with
   (bool_fun_of_bool_expr (univl be l)
      (fun y : BDDvar =>
       match Neqb a y with
       | true => true
       | false => var_env'_to_env ve y
       end)).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  assumption.  apply (bool_fun_of_be_ext (univl be l)).  intros.
(* Goal: @eq bool (var_env'_to_env ve b) (var_env'_to_env ve' b) *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (Neg b)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (Neg b) ve) (eval_be' (Neg b) ve') *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b0 ve) (eval_be' b0 ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (Or b b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (Or b b0) ve) (eval_be' (Or b b0) ve') *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b0 ve) (eval_be' b0 ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (ANd b b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (ANd b b0) ve) (eval_be' (ANd b b0) ve') *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b0 ve) (eval_be' b0 ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (Impl b b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (Impl b b0) ve) (eval_be' (Impl b b0) ve') *)
(* Goal: forall (b : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b ve) (eval_be' b ve')) (b0 : bool_expr) (_ : forall (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x b0) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' b0 ve) (eval_be' b0 ve')) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x (Iff b b0)) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' (Iff b b0) ve) (eval_be' (Iff b b0) ve') *)
  unfold var_env'_to_env in |- *.  rewrite (N_of_nat_of_N x).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (Neqb_comm a x).  reflexivity.  intros.
(* Goal: forall _ : @eq bool (Nat.leb N (N.to_nat x)) false, @eq bool (ve' (N.to_nat x)) (if Nat.leb N (N.to_nat x) then ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N)) else false) *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (Neqb (N_of_nat n) a)).  intro y0.  rewrite y0 in H4.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  discriminate.  intro y0.  rewrite y0 in H4.  elim (H2 _ H4).  intro.
(* Goal: @In BinNums.N (N.of_nat n) (lx' N) *)
(* Goal: @eq bool (eval_be' (ANd t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- H5 in y0.  rewrite (Neqb_correct a) in y0.  discriminate.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  trivial.  intros.  elim (sumbool_of_bool (Neqb (N_of_nat n) a)).  intro y0.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply no_dup_cons_no_in.  rewrite (Neqb_complete _ _ y0).  assumption.  
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intro y0.  rewrite y0 in H1.  unfold not in |- *; intro.  apply (H0 _ H1).  auto.  
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply no_dup_cons_no_dup with (a := a).  assumption.  unfold eval_be' in |- *.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (bool_fun_of_be_ext be).  intros.  unfold var_env'_to_env, var_env'_or in |- *.
(* Goal: forall _ : @eq bool (Nat.leb N (N.to_nat x)) false, @eq bool (ve' (N.to_nat x)) (if Nat.leb N (N.to_nat x) then ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N)) else false) *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (N_of_nat_of_N x).  elim (sumbool_of_bool (Neqb x a)).  intro y0.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite y0.  simpl in |- *.  rewrite (Neqb_complete _ _ y0).  rewrite y.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  auto with bool.  intro y0.  rewrite y0.  reflexivity.  intro y.  elim (H be ve).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  clear H4.  apply H3.  unfold eval_be' in |- *.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply forall_lemma1 with (a := a).  assumption.  intros.  elim (H2 _ H4).  intro.
(* Goal: @In BinNums.N (N.of_nat n) l *)
(* Goal: forall _ : @In BinNums.N (N.of_nat n) l, @In BinNums.N (N.of_nat n) l *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) l) *)
(* Goal: no_dup_list ad l *)
(* Goal: forall _ : forall (ve' : var_env') (_ : forall (n : nat) (_ : @eq bool (ve' n) true), or (@eq BinNums.N a (N.of_nat n)) (@In BinNums.N (N.of_nat n) l)), @eq bool (eval_be' be (var_env'_or ve ve')) true, @eq bool (eval_be' (forall_ a (univl be l)) ve) true *)
  rewrite H5 in y.  rewrite (nat_of_N_of_nat n) in y.  rewrite y in H4.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  discriminate.  auto.  intros.  unfold not in |- *; intro.  apply (H0 _ H3).  auto.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply no_dup_cons_no_dup with (a := a).  assumption.  intros.  unfold eval_be' in |- *.
(* Goal: @eq bool (bool_fun_of_bool_expr (forall_ a (univl be l)) (var_env'_to_env ve)) true *)
  rewrite (forall_OK a (univl be l) (var_env'_to_env ve)).
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold bool_fun_forall in |- *.  unfold bool_fun_and in |- *.  apply andb_true_intro.  split.
(* Goal: @eq bool (bool_fun_restrict (bool_fun_of_bool_expr (univl be l)) a false (var_env'_to_env ve)) true *)
  unfold bool_fun_restrict in |- *.
  elim
   (H be
      (fun n : nat =>
       match Neqb (N_of_nat n) a with
       | true => true
       | false => ve n
       end)).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  clear H2.
  replace
   (bool_fun_of_bool_expr (univl be l) (augment (var_env'_to_env ve) a true))
   with
   (eval_be' (univl be l)
      (fun n : nat =>
       match Neqb (N_of_nat n) a with
       | true => true
       | false => ve n
       end)).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply H3.  intros.
  replace
   (eval_be' be
      (var_env'_or
         (fun n : nat =>
          match Neqb (N_of_nat n) a with
          | true => true
          | false => ve n
          end) ve')) with
   (eval_be' be
      (var_env'_or ve
         (fun n : nat =>
          match Neqb (N_of_nat n) a with
          | true => true
          | false => ve' n
          end))).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply H1.  intros.  elim (sumbool_of_bool (Neqb (N_of_nat n) a)).  intro y.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  left.  rewrite (Neqb_complete _ _ y).  reflexivity.  intro y.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite y in H4.  right.  apply H2.  assumption.  unfold eval_be' in |- *.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (bool_fun_of_be_ext be).  intros.  unfold var_env'_to_env, var_env'_or in |- *.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (N_of_nat_of_N x).  elim (sumbool_of_bool (Neqb x a)).  intro y.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite y.  auto with bool.  intro y.  rewrite y.  reflexivity.
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve ve')) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold eval_be' in |- *.  unfold var_env'_to_env in |- *.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (bool_fun_of_be_ext (univl be l)).  intro.  rewrite (N_of_nat_of_N x).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold augment in |- *.  rewrite (Neqb_comm a x).  reflexivity.  intros.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (Neqb (N_of_nat n) a)).  intro y.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply no_dup_cons_no_in.  rewrite (Neqb_complete _ _ y).  assumption.  
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  intro y.  rewrite y in H2.  exact (fun x => H0 _ H2 (or_intror _ x)).  
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply no_dup_cons_no_dup with (a := a).  assumption.  unfold bool_fun_restrict in |- *.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (H be ve).  intros.  clear H2.
  replace
   (bool_fun_of_bool_expr (univl be l) (augment (var_env'_to_env ve) a false))
   with (eval_be' (univl be l) ve).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply H3.  intros.  apply H1.  intros.  auto.  unfold eval_be' in |- *.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (bool_fun_of_be_ext (univl be l)).  intro.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_to_env, augment in |- *.  elim (sumbool_of_bool (Neqb a x)).  intro y.
(* Goal: @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite y.  rewrite <- (Neqb_complete _ _ y).  apply not_true_is_false.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold not in |- *.  intro.  elim (H0 (nat_of_N a)).  assumption.  left.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (N_of_nat_of_N a).  reflexivity.  intro y.  rewrite y.  reflexivity.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  exact (fun x => H0 _ H2 (or_intror _ x)).
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply no_dup_cons_no_dup with (a := a).  assumption.
Qed.

Lemma bool_fun_of_be_ext1 :
 forall (be : bool_expr) (ve ve' : var_env'),
 (forall x : ad,
  be_x_free x be = true -> ve (nat_of_N x) = ve' (nat_of_N x)) ->
 eval_be' be ve = eval_be' be ve'.
Proof.
(* Goal: forall (be : bool_expr) (ve ve' : var_env') (_ : forall (x : ad) (_ : @eq bool (be_x_free x be) true), @eq bool (ve (N.to_nat x)) (ve' (N.to_nat x))), @eq bool (eval_be' be ve) (eval_be' be ve') *)
  simple induction be.  reflexivity.  reflexivity.  intros.  simpl in H.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold eval_be' in |- *.  simpl in |- *.  unfold bool_fun_var in |- *.  unfold var_env'_to_env in |- *.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (H b).  reflexivity.  apply Neqb_correct.  simpl in |- *.  intros.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold eval_be' in |- *.  simpl in |- *.  unfold eval_be' in H.  unfold bool_fun_neg in |- *.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (H ve ve' H0).  reflexivity.  unfold eval_be' in |- *.  simpl in |- *.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold bool_fun_or in |- *.  intros.  rewrite (H ve ve').  rewrite (H0 ve ve').
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  intros.  apply H1.  rewrite H2.  auto with bool.  intros.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply H1.  rewrite H2.  auto with bool.  unfold eval_be' in |- *.  simpl in |- *.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold bool_fun_and in |- *.  simpl in |- *.  intros.  rewrite (H ve ve').
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (H0 ve ve').  reflexivity.  intros.  apply H1.  rewrite H2.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  auto with bool.  intros.  apply H1.  rewrite H2.  auto with bool.  
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold eval_be' in |- *.  simpl in |- *.  unfold bool_fun_impl in |- *.  intros.  rewrite (H ve ve').
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (H0 ve ve').  reflexivity.  intros.  apply H1.  rewrite H2.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  auto with bool.  intros.  apply H1.  rewrite H2.  auto with bool.  
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold eval_be' in |- *.  simpl in |- *.  unfold bool_fun_iff in |- *.  intros.  rewrite (H ve ve').
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (H0 ve ve').  reflexivity.  intros.  apply H1.  rewrite H2.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  auto with bool.  intros.  apply H1.  rewrite H2.  auto with bool.
Qed.


Lemma no_dup_lx'_1 : forall n : nat, no_dup_list _ (lx'_1 N n).
Proof.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  simple induction n.  simpl in |- *.  apply no_dup_nil.  simpl in |- *.  intros.  apply no_dup_cons.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold not in |- *; intro.  elim (in_lx'_1_conv _ _ _ H0).  intros.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (lt_irrefl _ H2).  assumption.
Qed.

Lemma mu_all_eval_semantics1 :
 forall t be : bool_expr,
 be_ok (var_lu 0 N) be ->
 forall ve : var_env',
 (forall n : nat, ve n = true -> var_lu 0 N (N_of_nat n) = true) ->
 eval_be' (mu_all_eval N t be) ve = true ->
 forall ve' : var_env',
 (forall n : nat, ve' n = true -> var_lu 0 N (N_of_nat n) = true) ->
 eval_be' t (var_env'_or ve (var_env'_dash ve')) = true ->
 eval_be' be ve' = true.
Proof.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  unfold mu_all_eval in H1.  rewrite (replacel_lemma2 be H) in H1.
(* Goal: @eq bool (eval_be' be ve') true *)
  rewrite (eval_dash_lemma1 be ve').
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (univl_semantics (lx' N) (Impl t (be_dash be)) ve).  intros.  clear H5.
  cut
   (eval_be' (Impl t (be_dash be)) (var_env'_or ve (var_env'_dash ve')) =
    true).
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intro.  cut (eval_be' (be_dash be) (var_env'_or ve (var_env'_dash ve')) = true).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intro.  rewrite <- H6.  apply bool_fun_of_be_ext1.  intros.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_or in |- *.  replace (ve (nat_of_N x)) with false.  reflexivity.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  symmetry  in |- *.  apply not_true_is_false.  unfold not in |- *; intro.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  cut (var_lu 0 N x = true).  cut (var_lu N (2 * N) x = true).  intros.
(* Goal: False *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: @eq bool (var_lu O N x) true *)
(* Goal: @eq bool (eval_be' (be_dash be) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_lu in H9, H10.  elim (andb_prop _ _ H9).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (andb_prop _ _ H10).  intros.  apply (lt_irrefl N).
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply le_lt_trans with (m := nat_of_N x).  apply leb_complete; assumption.
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold lt in |- *.  apply leb_complete; assumption.  
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: @eq bool (var_lu O N x) true *)
(* Goal: @eq bool (eval_be' (be_dash be) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (be_ok_be_x_free (var_lu N (2 * N)) (be_dash be)).
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply dash_be_ok.  assumption.  assumption.  rewrite <- (N_of_nat_of_N x).
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply H0.  assumption.  unfold eval_be' in |- *.  unfold eval_be' in H5.  simpl in H5.
(* Goal: @eq bool (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve (var_env'_dash ve')))) true *)
(* Goal: @eq bool (eval_be' (Impl t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold bool_fun_impl in H5.  unfold eval_be' in H3.  rewrite H3 in H5.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  simpl in H5.  assumption.  apply H4.  assumption.  intros.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_dash in H5.  elim (sumbool_of_bool (leb N n)).  intro y.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite y in H5.  apply in_lx'.  apply leb_complete; assumption.  
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  cut (var_lu 0 N (N_of_nat (n - N)) = true).  unfold var_lu in |- *.  intro.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (andb_prop _ _ H6).  intros.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (nat_of_N_of_nat (n - N)) in H8.  simpl in |- *.
(* Goal: le (S n) (Init.Nat.add N (Init.Nat.add N O)) *)
(* Goal: forall _ : @eq bool (Nat.leb N n) false, @In BinNums.N (N.of_nat n) (lx' N) *)
(* Goal: @eq bool (eval_be' (ANd t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- (plus_n_O N).  replace n with (n - N + N).
(* Goal: le (S (Init.Nat.add (Init.Nat.sub n N) N)) (Init.Nat.add N N) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub n N) N) n *)
(* Goal: forall _ : @eq bool (Nat.leb N n) false, @In BinNums.N (N.of_nat n) (lx' N) *)
(* Goal: @eq bool (eval_be' (ANd t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  replace (S (n - N + N)) with (S (n - N) + N).
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply plus_le_compat.  apply leb_complete; assumption.  apply le_n.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  rewrite (plus_comm (n - N) N).  symmetry  in |- *.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply le_plus_minus.  apply leb_complete; assumption.  apply H2.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  assumption.  intro y.  rewrite y in H5.  discriminate.  intros.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold not in |- *; intro.  unfold lx' in H5.  elim (in_lx'_1_conv N N n H5).  intro.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intro.  unfold var_lu in H0.  elim (andb_prop _ _ (H0 n H4)).  intros.
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (lt_irrefl N).  apply le_lt_trans with (m := n).  assumption.  unfold lt in |- *.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (nat_of_N_of_nat n) in H9.  apply leb_complete; assumption.
(* Goal: no_dup_list ad (lx' N) *)
  unfold lx' in |- *.  apply no_dup_lx'_1.
Qed.

Lemma mu_ex_eval_semantics1 :
 forall t be : bool_expr,
 be_ok (var_lu 0 N) be ->
 forall ve : var_env',
 (forall n : nat, ve n = true -> var_lu 0 N (N_of_nat n) = true) ->
 eval_be' (mu_ex_eval N t be) ve = true ->
 exists ve' : var_env',
   (forall n : nat, ve' n = true -> var_lu 0 N (N_of_nat n) = true) /\
   eval_be' t (var_env'_or ve (var_env'_dash ve')) = true /\
   eval_be' be ve' = true.
Proof.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  unfold mu_ex_eval in H1.  rewrite (replacel_lemma2 be H) in H1.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (exl_semantics (lx' N) (ANd t (be_dash be)) ve).  intros.  clear H3.
(* Goal: forall (x : var_env') (_ : and (forall (n : nat) (_ : @eq bool (x n) true), @In BinNums.N (N.of_nat n) (lx' N)) (@eq bool (eval_be' (ANd t (be_dash be)) (var_env'_or ve x)) true)), @ex var_env' (fun ve' : var_env' => and (forall (n : nat) (_ : @eq bool (ve' n) true), @eq bool (var_lu O N (N.of_nat n)) true) (and (@eq bool (eval_be' t (var_env'_or ve (var_env'_dash ve'))) true) (@eq bool (eval_be' be ve') true))) *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (H2 H1).  intros ve' H3.  inversion H3.  clear H2 H3.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  split with (fun n : nat => ve' (N + n)).  split.  intros.  unfold var_lu in |- *.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply andb_true_intro.  rewrite (nat_of_N_of_nat n).  split.
(* Goal: @eq bool (Nat.leb (S n) N) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_correct.  apply le_O_n.  elim (in_lx'_1_conv _ _ _ (H4 _ H2)).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  apply leb_correct.  unfold lt in H6.
(* Goal: le (S n) N *)
(* Goal: and (@eq bool (eval_be' t (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n))))) true) (@eq bool (eval_be' be (fun n : nat => ve' (Init.Nat.add N n))) true) *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (Splus_nm N n) in H6.  rewrite (plus_Snm_nSm N n) in H6.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (fun p n m : nat => plus_le_reg_l n m p) with (p := N).  assumption.  unfold eval_be' in H5.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  simpl in H5.  unfold bool_fun_and in H5.  elim (andb_prop _ _ H5).  intros.
(* Goal: and (@eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (@eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true) *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  split.  rewrite <- H2.  unfold eval_be' in |- *.  apply (bool_fun_of_be_ext t).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_to_env, var_env'_or, var_env'_dash in |- *.  intros.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (leb N (nat_of_N x))).  intro y.  rewrite y.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- (le_plus_minus N (nat_of_N x)).  reflexivity.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_complete; assumption.  intro y.  rewrite y.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  replace (ve' (nat_of_N x)) with false.  reflexivity.  symmetry  in |- *.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply not_true_is_false.  unfold not in |- *; intro.  unfold lx' in H4.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (in_lx'_1_conv _ _ _ (H4 _ H6)).  intros.
(* Goal: @In BinNums.N (N.of_nat n) (lx' N) *)
(* Goal: @eq bool (eval_be' (ANd t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (leb_correct _ _ H7) in y; discriminate.
(* Goal: @eq bool (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve'))) (eval_be' be (fun n : nat => ve' (Init.Nat.add N n))) *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (eval_dash_lemma1 be (fun n : nat => ve' (N + n))).  rewrite <- H3.
(* Goal: @eq bool (eval_be' t (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n))))) (eval_be' t (var_env'_or ve ve')) *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  fold (eval_be' (be_dash be) (var_env'_or ve ve')) in |- *.  apply bool_fun_of_be_ext1.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  unfold var_env'_or in |- *.  unfold var_env'_dash in |- *.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  cut (var_lu N (2 * N) x = true).  unfold var_lu in |- *.  intro.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (andb_prop _ _ H7).  intros.  rewrite H8.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  replace (ve (nat_of_N x)) with false.  simpl in |- *.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- (le_plus_minus N (nat_of_N x)).  reflexivity.
(* Goal: le N (N.to_nat x) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_complete.  assumption.  symmetry  in |- *.  apply not_true_is_false.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold not in |- *; intro.  unfold var_lu in H0.  elim (andb_prop _ _ (H0 _ H10)).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  rewrite (N_of_nat_of_N x) in H12.  apply (lt_irrefl N).
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply le_lt_trans with (m := nat_of_N x).  apply leb_complete; assumption.    unfold lt in |- *.  apply leb_complete; assumption.  
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply be_ok_be_x_free with (be := be_dash be).  apply dash_be_ok.  assumption.  
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  assumption.  intros.  unfold lx' in |- *.  unfold not in |- *; intro.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (in_lx'_1_conv _ _ _ H3).  intros.  unfold var_lu in H0.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (andb_prop _ _ (H0 _ H2)).  rewrite (nat_of_N_of_nat n).  intros.
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (lt_irrefl N).  apply le_lt_trans with (m := n).  assumption.  unfold lt in |- *.
(* Goal: le N (N.to_nat x) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_complete.  assumption.  unfold lx' in |- *.  apply no_dup_lx'_1.
Qed.

Lemma mu_ex_eval_semantics2 :
 forall t be : bool_expr,
 be_ok (var_lu 0 N) be ->
 forall ve : var_env',
 (forall n : nat, ve n = true -> var_lu 0 N (N_of_nat n) = true) ->
 (exists ve' : var_env',
    (forall n : nat, ve' n = true -> var_lu 0 N (N_of_nat n) = true) /\
    eval_be' t (var_env'_or ve (var_env'_dash ve')) = true /\
    eval_be' be ve' = true) -> eval_be' (mu_ex_eval N t be) ve = true.
Proof.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold mu_ex_eval in |- *.  intros.  rewrite (replacel_lemma2 be H).  elim H1.
(* Goal: @eq bool (eval_be' (exl (ANd t (be_dash be)) (lx' N)) ve) true *)
  clear H1.  intros ve' H1.  inversion H1.  inversion H3.  clear H3 H1.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (exl_semantics (lx' N) (ANd t (be_dash be)) ve).  intros.  clear H1.
(* Goal: and (@eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (@eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true) *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply H3.  clear H3.  split with (var_env'_dash ve').  split.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_dash in |- *.  intros.  elim (sumbool_of_bool (leb N n)).  intros y.
(* Goal: le N (N.to_nat x) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply in_lx'.  apply leb_complete.  assumption.  rewrite y in H1.
(* Goal: le (S n) (Init.Nat.mul (S (S O)) N) *)
(* Goal: forall _ : @eq bool (Nat.leb N n) false, @In BinNums.N (N.of_nat n) (lx' N) *)
(* Goal: @eq bool (eval_be' (ANd t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_lu in H2.  elim (andb_prop _ _ (H2 _ H1)).
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (nat_of_N_of_nat (n - N)).  intros.  simpl in |- *.
(* Goal: le (S n) (Init.Nat.add N (Init.Nat.add N O)) *)
(* Goal: forall _ : @eq bool (Nat.leb N n) false, @In BinNums.N (N.of_nat n) (lx' N) *)
(* Goal: @eq bool (eval_be' (ANd t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- (plus_n_O N).  replace n with (n - N + N).
(* Goal: le (S (Init.Nat.add (Init.Nat.sub n N) N)) (Init.Nat.add N N) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub n N) N) n *)
(* Goal: forall _ : @eq bool (Nat.leb N n) false, @In BinNums.N (N.of_nat n) (lx' N) *)
(* Goal: @eq bool (eval_be' (ANd t (be_dash be)) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  replace (S (n - N + N)) with (S (n - N) + N).
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply plus_le_compat.  apply leb_complete; assumption.  apply le_n.  
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  rewrite (plus_comm (n - N) N).  symmetry  in |- *.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply le_plus_minus.  apply leb_complete; assumption.  intro y.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite y in H1.  discriminate.  unfold eval_be' in |- *.  simpl in |- *.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold bool_fun_and in |- *.  apply andb_true_intro.  split.  exact H4.  
(* Goal: @eq bool (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve (var_env'_dash ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  fold (eval_be' (be_dash be) (var_env'_or ve (var_env'_dash ve'))) in |- *.
(* Goal: @eq bool (eval_be' (be_dash be) (var_env'_or ve (var_env'_dash ve'))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (eval_dash_lemma1 be ve') in H5.  rewrite <- H5.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (bool_fun_of_be_ext1 (be_dash be)).  intros.  unfold var_env'_or in |- *.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  replace (ve (nat_of_N x)) with false.  reflexivity.  symmetry  in |- *.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply not_true_is_false.  unfold not in |- *; intro.  unfold var_lu in H0.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (andb_prop _ _ (H0 _ H3)).  rewrite (N_of_nat_of_N x).  intros.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (andb_prop _ _ (be_ok_be_x_free _ _ (dash_be_ok _ H) _ H1)).  intros.
(* Goal: False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (lt_irrefl N).  apply le_lt_trans with (m := nat_of_N x).
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_complete; assumption.  unfold lt in |- *.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_complete; assumption.  unfold not in |- *; intros.  unfold lx' in H3.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (in_lx'_1_conv _ _ _ H3).  intros.  unfold var_lu in H0.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (andb_prop _ _ (H0 _ H1)).  rewrite (nat_of_N_of_nat n).  intros.
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply (lt_irrefl N).  apply le_lt_trans with (m := n).  assumption.  unfold lt in |- *.
(* Goal: le N (N.to_nat x) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_complete.  assumption.  unfold lx' in |- *.  apply no_dup_lx'_1.
Qed.

Lemma mu_all_eval_semantics2 :
 forall t be : bool_expr,
 be_ok (var_lu 0 N) be ->
 forall ve : var_env',
 (forall n : nat, ve n = true -> var_lu 0 N (N_of_nat n) = true) ->
 (forall ve' : var_env',
  (forall n : nat, ve' n = true -> var_lu 0 N (N_of_nat n) = true) ->
  eval_be' t (var_env'_or ve (var_env'_dash ve')) = true ->
  eval_be' be ve' = true) -> eval_be' (mu_all_eval N t be) ve = true.
Proof.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold mu_all_eval in |- *.  intros.  rewrite (replacel_lemma2 be H).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (univl_semantics (lx' N) (Impl t (be_dash be)) ve).  intros.  clear H2.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply H3.  intros.  clear H3.  unfold eval_be' in |- *.  simpl in |- *.  unfold bool_fun_impl in |- *.
  elim
   (sumbool_of_bool
      (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve')))).
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  intro y.  rewrite y.  simpl in |- *.  unfold eval_be' in H1.
(* Goal: @eq bool (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve'))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- (H1 (fun n : nat => ve' (N + n))).
(* Goal: @eq bool (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr be (var_env'_to_env (fun n : nat => ve' (Init.Nat.add N n)))) *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  fold (eval_be' be (fun n : nat => ve' (N + n))) in |- *.
(* Goal: @eq bool (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve'))) (eval_be' be (fun n : nat => ve' (Init.Nat.add N n))) *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (eval_dash_lemma1 be (fun n : nat => ve' (N + n))).
(* Goal: @eq bool (eval_be' t (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n))))) (eval_be' t (var_env'_or ve ve')) *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  fold (eval_be' (be_dash be) (var_env'_or ve ve')) in |- *.  apply bool_fun_of_be_ext1.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  intros.  unfold var_env'_or in |- *.  unfold var_env'_dash in |- *.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  cut (var_lu N (2 * N) x = true).  unfold var_lu in |- *.  intro.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (andb_prop _ _ H4).  intros.  rewrite H5.
(* Goal: @eq bool (orb false (ve' (N.to_nat x))) (ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N))) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  replace (ve (nat_of_N x)) with false.  simpl in |- *.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- (le_plus_minus N (nat_of_N x)).  reflexivity.  
(* Goal: le N (N.to_nat x) *)
(* Goal: @eq bool false (ve (N.to_nat x)) *)
(* Goal: @eq bool (var_lu N (Init.Nat.mul (S (S O)) N) x) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve' (Init.Nat.add N n)) true), @eq bool (var_lu O N (N.of_nat n)) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_complete.  assumption.  symmetry  in |- *.  apply not_true_is_false.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold not in |- *; intro.  unfold var_lu in H0.  elim (andb_prop _ _ (H0 _ H7)).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  intros.  rewrite (N_of_nat_of_N x) in H9.  apply (lt_irrefl N).
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply le_lt_trans with (m := nat_of_N x).  apply leb_complete; assumption.  
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold lt in |- *.  apply leb_complete; assumption.  
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply be_ok_be_x_free with (be := be_dash be).  apply dash_be_ok.  assumption.  
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  assumption.  intros.  unfold var_lu in |- *.  apply andb_true_intro.  split.
(* Goal: @eq bool (Nat.leb (S n) N) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_correct.  apply le_O_n.  rewrite (nat_of_N_of_nat n).
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold lx' in H2.  elim (in_lx'_1_conv _ _ _ (H2 _ H3)).  intros.
(* Goal: @eq bool (Nat.leb (S n) N) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold lt in H5.  rewrite (plus_comm N n) in H5.  rewrite (Splus_nm n N) in H5.
(* Goal: @eq bool (Nat.leb (S n) N) true *)
(* Goal: @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n)))))) true *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_correct.  apply (fun p n m : nat => plus_le_reg_l n m p) with (p := N).
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (plus_comm N (S n)).  assumption.  rewrite <- y.
  fold
   (eval_be' t (var_env'_or ve (var_env'_dash (fun n : nat => ve' (N + n)))))
   in |- *.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  fold (eval_be' t (var_env'_or ve ve')) in |- *.  apply bool_fun_of_be_ext1.  intros.
(* Goal: @eq bool (var_env'_or ve (var_env'_dash (fun n : nat => ve' (Init.Nat.add N n))) (N.to_nat x)) (var_env'_or ve ve' (N.to_nat x)) *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  unfold var_env'_or in |- *.
  replace (var_env'_dash (fun n : nat => ve' (N + n)) (nat_of_N x)) with
   (ve' (nat_of_N x)).
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  unfold var_env'_dash in |- *.
(* Goal: forall _ : @eq bool (Nat.leb N (N.to_nat x)) false, @eq bool (ve' (N.to_nat x)) (if Nat.leb N (N.to_nat x) then ve' (Init.Nat.add N (Init.Nat.sub (N.to_nat x) N)) else false) *)
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (sumbool_of_bool (leb N (nat_of_N x))).  intro y0.  rewrite y0.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite <- (le_plus_minus N (nat_of_N x)).  reflexivity.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply leb_complete; assumption.  intro y0.  rewrite y0.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  apply not_true_is_false.  unfold not in |- *; intro.  unfold lx' in H2.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (in_lx'_1_conv _ _ _ (H2 _ H4)).  intros.
(* Goal: forall _ : @eq bool (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) false, @eq bool (implb (bool_fun_of_bool_expr t (var_env'_to_env (var_env'_or ve ve'))) (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (leb_correct _ _ H5) in y0; discriminate.  intro y.  rewrite y.
(* Goal: @eq bool (implb false (bool_fun_of_bool_expr (be_dash be) (var_env'_to_env (var_env'_or ve ve')))) true *)
(* Goal: forall (n : nat) (_ : @eq bool (ve n) true), not (@In BinNums.N (N.of_nat n) (lx' N)) *)
(* Goal: no_dup_list ad (lx' N) *)
  reflexivity.  intros.  unfold not in |- *; intro.  unfold lx' in H3.
(* Goal: forall _ : lt n (Init.Nat.add N N), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (in_lx'_1_conv N N n H3).  intro.  intro.  unfold var_lu in H0.
(* Goal: forall (_ : @eq bool (Nat.leb O (N.to_nat (N.of_nat n))) true) (_ : @eq bool (Nat.leb (S (N.to_nat (N.of_nat n))) N) true), False *)
(* Goal: no_dup_list ad (lx' N) *)
  elim (andb_prop _ _ (H0 n H2)).  intros.  apply (lt_irrefl N).
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  apply le_lt_trans with (m := n).  assumption.  unfold lt in |- *.
(* Goal: le N n *)
(* Goal: lt n N *)
(* Goal: no_dup_list ad (lx' N) *)
  rewrite (nat_of_N_of_nat n) in H7.  apply leb_complete; assumption.
(* Goal: no_dup_list ad (lx' N) *)
  unfold lx' in |- *.  apply no_dup_lx'_1.
Qed.

End New.