Require Import Arith List.
Require Import BellantoniCook.Lib BellantoniCook.Bitstring BellantoniCook.BC BellantoniCook.BCI.

Fixpoint conv n s (e : BCI) : BC :=
  match e with
    | zeroI => comp n s zero nil nil
    | projIn i => proj n s i
    | projIs i => proj n s (n + i)
    | succI b => comp n s (succ b) nil [proj n s n]
    | predI => comp n s pred nil [proj n s n]
    | condI => comp n s cond nil 
      [proj n s n; proj n s (S n); proj n s (S (S n)); proj n s (S (S (S n)))]
    | recI g h0 h1 => rec (conv (n-1) s g) 
                          (conv n (S s) h0) 
                          (conv n (S s) h1)
    | compI g ln ls =>
      comp n s (conv (length ln) (length ls) g) 
       (map (conv n 0) ln) (map (conv n s) ls) 
  end.

Definition zeroI_e := compI zeroI nil nil.

Definition leftI (d:nat)(x:TypeI) : nat :=
 match x with
 | I n _ => n
 | E _ => d
 end.

Lemma inf_list_maxl_l : forall l n s,
 inf_list l = I n s ->
 n = maxl (map (leftI 0) l).
Proof.
 induction l; intros.
 compute in *.
 injection H; auto. 
 simpl in *.
 destruct a; simpl in *.
 destruct (inf_list l).
 injection H; clear H; intros; subst.
(* Goal: @eq (list bool) (semI e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
 f_equal.
 eapply IHl.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (E (Enat (S (S (S Datatypes.O))))) (E err')) *)
 eauto.
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
 discriminate.
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
 discriminate.
Qed.

Definition rightI (d:nat)(x:TypeI) : nat :=
 match x with
 | I _ n => n
 | E _ => d
 end.

Lemma inf_list_maxl_r : forall l n s,
 inf_list l = I n s ->
 s = maxl (map (rightI 0) l).
Proof.
 induction l; intros.
 compute in *.
 injection H; auto. 
 simpl in *.
 destruct a; simpl in *.
 destruct (inf_list l).
 injection H; clear H; intros; subst.
(* Goal: @eq (list bool) (semI e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
 f_equal.
 eapply IHl.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (E (Enat (S (S (S Datatypes.O))))) (E err')) *)
 eauto.
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
 discriminate.
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
 discriminate.
Qed.

Lemma in_inf_list_le_l l n s n' s' :
 In (I n' s') l -> inf_list l = I n s -> n' <= n.
Proof.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
intros.
(* Goal: le n' n *)
apply inf_list_maxl_l in H0.
(* Goal: le s' s *)
subst.
(* Goal: le n' (maxl (@map TypeI nat (leftI Datatypes.O) l)) *)
apply in_map with (f:=leftI 0) in H.
induction (map (leftI 0) l); simpl in *.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (I Datatypes.O Datatypes.O) (E err')) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (unionI a (inf_list l)) (E err')) *)
elim H.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (unionI a (inf_list l)) (E err')) *)
destruct H.
(* Goal: le s' (Init.Nat.max a (maxl l0)) *)
(* Goal: le s' (Init.Nat.max a (maxl l0)) *)
subst a.
(* Goal: le s' (Init.Nat.max s' (maxl l0)) *)
(* Goal: le s' (Init.Nat.max a (maxl l0)) *)
apply maxl_cons.
(* Goal: le s' (Init.Nat.max a (maxl l0)) *)
apply le_maxl_cons.
(* Goal: le s' (maxl l0) *)
tauto.
Qed.

Lemma in_inf_list_le_r l n s n' s' :
 In (I n' s') l -> inf_list l = I n s -> s' <= s.
Proof.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
intros.
(* Goal: le s' s *)
apply inf_list_maxl_r in H0.
(* Goal: le s' s *)
subst.
(* Goal: le s' (maxl (@map TypeI nat (rightI Datatypes.O) l)) *)
apply in_map with (f:=rightI 0) in H.
induction (map (rightI 0) l); simpl in *.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (I Datatypes.O Datatypes.O) (E err')) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (unionI a (inf_list l)) (E err')) *)
elim H.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (unionI a (inf_list l)) (E err')) *)
destruct H.
(* Goal: le s' (Init.Nat.max a (maxl l0)) *)
(* Goal: le s' (Init.Nat.max a (maxl l0)) *)
subst a.
(* Goal: le s' (Init.Nat.max s' (maxl l0)) *)
(* Goal: le s' (Init.Nat.max a (maxl l0)) *)
apply maxl_cons.
(* Goal: le s' (Init.Nat.max a (maxl l0)) *)
apply le_maxl_cons.
(* Goal: le s' (maxl l0) *)
tauto.
Qed.

Lemma in_inf_list_le l n s n' s' :
 In (I n' s') l -> inf_list l = I n s -> n' <= n /\ s' <= s.
Proof.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
intros.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
generalize H0; intros.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (E (Enat (S (S (S Datatypes.O))))) (E err')) *)
eapply in_inf_list_le_r in H0; eauto.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (E (Enat (S (S (S Datatypes.O))))) (E err')) *)
eapply in_inf_list_le_l in H1; eauto.
Qed.

Lemma in_inf_list_err : forall l err,
 In (E err) l -> exists err', inf_list l = E err'.
Proof.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
 induction l; simpl; intros.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (I Datatypes.O Datatypes.O) (E err')) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (unionI a (inf_list l)) (E err')) *)
 elim H.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (unionI a (inf_list l)) (E err')) *)
 destruct H.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (unionI a (inf_list l)) (E err')) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (unionI a (inf_list l)) (E err')) *)
 subst; simpl.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (E (Enat (S (S (S Datatypes.O))))) (E err')) *)
 eauto.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (unionI a (inf_list l)) (E err')) *)
 destruct (IHl err H).
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (unionI a (inf_list l)) (E err')) *)
 rewrite H0; simpl.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (unionI a (E x)) (E err')) *)
 destruct a; simpl.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (E (Enat (S (S (S Datatypes.O))))) (E err')) *)
 eauto.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (E (Enat (S (S (S Datatypes.O))))) (E err')) *)
 eauto.
Qed.

Lemma in_inf_list_err_conv : forall l err, 
  inf_list l = E err ->
  exists err', In (E err') l.
Proof.
(* Goal: forall (l : list TypeI) (err : ErrorI) (_ : @eq TypeI (inf_list l) (E err)), @ex ErrorI (fun err' : ErrorI => @In TypeI (E err') l) *)
 induction l; simpl; intros; trivial.
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
 discriminate.
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI a (E err')) (@In TypeI (E err') l)) *)
 destruct a; simpl in H.
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
 case_eq (inf_list l); intros; rewrite H0 in H.
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
 discriminate.
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
 destruct (IHl e); trivial.
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
 exists x; auto.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (E (Enat (S (S (S Datatypes.O))))) (E err')) *)
 eexists; eauto.
Qed.

Lemma inf_list_ex : forall l e n s,
 In e l -> inf_list (map inf l) = I n s ->
   exists n', exists s', n' <= n /\ s' <= s /\ inf e = I n' s'.
Proof.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
intros.
case_eq (inf e).
intros n' s' H1.
exists n'.
exists s'.
split.
apply in_inf_list_le_l with (l:=map inf l) (s:=s) (s':=s').
rewrite <- H1.
apply in_map.
assumption.
assumption.
split.
apply in_inf_list_le_r with (l:=map inf l) (n:=n) (n':=n').
rewrite <- H1.
apply in_map.
assumption.
assumption.
reflexivity.
intros err H1.
assert (In (E err) (map inf l)).
rewrite  <- H1.
apply in_map.
assumption.
contradict H0.
intro.
edestruct in_inf_list_err.
(* Goal: @ex ErrorI (fun err' : ErrorI => @eq TypeI (E (Enat (S (S (S Datatypes.O))))) (E err')) *)
eauto.
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
rewrite H0 in H3; discriminate.
Qed.

Opaque maxl.

Lemma inf_correct : forall (e : BCI) n s n' s',
  n' <= n ->
  s' <= s ->
  inf e = I n' s' ->
  arities (conv n s e) = ok_arities n s.
Proof.
(* Goal: forall (e : BCI) (vnl vsl : list (list bool)) (n s n' s' : nat) (_ : le n' n) (_ : le s' s) (_ : @eq TypeI (inf e) (I n' s')), @eq (list bool) (sem (conv n s e) vnl vsl) (semI e vnl vsl) *)
  induction e using BCI_ind2; simpl; intros; trivial.
  
(* Goal: le s' s *)
  injection H1; intros; subst.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  case_eq (n + s); intros.
  contradict H2; omega.
  case_eq (leb i n0); intros; trivial.
  apply leb_complete_conv in H3.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.

(* Goal: le s' s *)
  injection H1; intros; subst.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  case_eq (n + s); intros.
  contradict H2; omega.
  case_eq (leb (n + i) n0); intros; trivial.
  apply leb_complete_conv in H3.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
  
(* Goal: le s' s *)
  injection H1; intros; subst.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  case_eq (n + s); intros.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  case_eq (leb n n0); intros; trivial; simpl.
  do 2 rewrite <- beq_nat_refl; simpl; trivial.
  apply leb_complete_conv in H3.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.

(* Goal: le s' s *)
  injection H1; intros; subst.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  case_eq (n + s); intros.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  case_eq (leb n n0); intros; trivial; simpl.
  do 2 rewrite <- beq_nat_refl; simpl; trivial.
  apply leb_complete_conv in H3.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.

(* Goal: le s' s *)
  injection H1; intros; subst.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  case_eq (n + s); intros.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  case_eq (leb n n0); intros; trivial; simpl.
  repeat rewrite <- beq_nat_refl; simpl; trivial.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  destruct n0; simpl.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  case_eq (leb n n0); intros; trivial; simpl.
  repeat rewrite <- beq_nat_refl; simpl; trivial.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  destruct n0; simpl.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  case_eq (leb n n0); intros; trivial; simpl.
  repeat rewrite <- beq_nat_refl; simpl; trivial.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  destruct n0; simpl.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  case_eq (leb n n0); intros; trivial; simpl.
  repeat rewrite <- beq_nat_refl; simpl; trivial.
  apply leb_complete_conv in H6.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
  apply leb_complete_conv in H5.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
  apply leb_complete_conv in H4.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
  apply leb_complete_conv in H3.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.

  case_eq (inf e1); [ intros n1 s1 He1 | intros ].
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
  2: rewrite H2 in H1; discriminate.
  rewrite He1 in H1.
  case_eq (inf e2); [ intros n2 s2 He2 | intros ].
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
  2: rewrite H2 in H1; discriminate.
  rewrite He2 in H1.
  case_eq (inf e3); [ intros n3 s3 He3 | intros ].
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
  2: rewrite H2 in H1; discriminate.
  rewrite He3 in H1.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  injection H1; intros.
  apply maxl_eq_le3 in H2.
  apply maxl_eq_le3 in H3.
  erewrite IHe1;[ | | | eauto ]; try omega.
  erewrite IHe2;[ | | | eauto ]; try omega.
  erewrite IHe3;[ | | | eauto ]; try omega.
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  destruct n.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
  replace (S n - 1) with n.
  do 4 rewrite <- beq_nat_refl; simpl; trivial.
(* Goal: le sa s *)
  omega.

  case_eq (inf e); intros; 
    rewrite H4 in H3; [ | discriminate ].
  case_eq (leb n0 (length rl)); intros;
  case_eq (leb n1 (length tl)); intros;
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
  rewrite H5, H6 in H3; try discriminate.
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl in H3.
  case_eq (inf_list (map inf rl)); intros;
    rewrite H7 in H3; [ | discriminate ].
  case_eq (inf_list (map inf tl)); intros;
    rewrite H8 in H3; [ | discriminate ].
  case_eq (beq_nat n3 0); intros; 
    rewrite H9 in H3; [ | discriminate ].
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  apply leb_complete in H5.
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  apply leb_complete in H6.
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  apply beq_nat_true in H9.  
(* Goal: le sa s *)
  erewrite IHe; [ | | | eauto]; try omega.
  do 2 rewrite map_length.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 2 rewrite <- beq_nat_refl; simpl.
(* Goal: le s' s *)
  injection H3; clear H3; intros; subst.
  assert (n2 <= max n2 n4 /\ n4 <= max n2 n4).
  split.
  apply Max.le_max_l.
  apply Max.le_max_r.
  replace (forallb 
    (fun ne : BC => aeq (arities ne) (ok_arities n 0))
    (map (conv n 0) rl)) with true.
  replace ( forallb 
    (fun se : BC => aeq (arities se) (ok_arities n s))
    (map (conv n s) tl)) with true.
  simpl; trivial.
  symmetry.
  eapply forallb_forall.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  intros.
  apply in_map_iff in H9.
  destruct H9 as (e' & H10 & H11).
(* Goal: le s' s *)
  subst.
  destruct (inf_list_ex _ _ _ _ H11 H8).
  destruct H9.
  erewrite H0.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl.
  do 2 rewrite <- beq_nat_refl; simpl; trivial.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  trivial.
  3: apply H9.
(* Goal: le sa s *)
  omega.
(* Goal: le sa s *)
  omega.
  symmetry.
  eapply forallb_forall.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  intros.
  apply in_map_iff in H9.
  destruct H9 as (e' & H10 & H11).
(* Goal: le s' s *)
  subst.
  destruct (inf_list_ex _ _ _ _ H11 H7).
  destruct H9.
  erewrite H.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl.
  rewrite <- beq_nat_refl; simpl; trivial.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  trivial.
  3: apply H9.
(* Goal: le sa s *)
  omega.
(* Goal: le sa s *)
  omega.
Qed.

Lemma conv_correct : forall (e : BCI) (vnl vsl : list bs) 
  n s n' s',
  n' <= n ->
  s' <= s ->
  inf e = I n' s' ->
  sem (conv n s e) vnl vsl = semI e vnl vsl.
Proof.
(* Goal: forall (e : BCI) (vnl vsl : list (list bool)) (n s n' s' : nat) (_ : le n' n) (_ : le s' s) (_ : @eq TypeI (inf e) (I n' s')), @eq (list bool) (sem (conv n s e) vnl vsl) (semI e vnl vsl) *)
  induction e using BCI_ind2; simpl; intros; trivial.

(* Goal: le s' s *)
  injection H1; clear H1; intros; subst.
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  destruct n.
(* Goal: le sa s *)
  contradict H; omega.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  case_eq (leb i n); intros; trivial.
(* Goal: @eq (list bool) (@nth (list bool) (Init.Nat.sub i (S n)) vsl (@nil bool)) (@nth (list bool) i vnl (@nil bool)) *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S m' => Nat.leb (Init.Nat.add n i) m' end then @nth (list bool) (Init.Nat.add n i) vnl (@nil bool) else @nth (list bool) (Init.Nat.sub (Init.Nat.add n i) n) vsl (@nil bool)) (@nth (list bool) i vsl (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  apply leb_complete_conv in H1.
(* Goal: le sa s *)
  contradict H; omega.

(* Goal: le s' s *)
  injection H1; clear H1; intros; subst.
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  destruct n.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  simpl; rewrite <- (minus_n_O i); trivial.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  case_eq (leb (S n + i) n); intros.  
(* Goal: @eq (list bool) (@nth (list bool) (Init.Nat.add (S n) i) vnl (@nil bool)) (@nth (list bool) i vsl (@nil bool)) *)
(* Goal: @eq (list bool) (@nth (list bool) (Init.Nat.sub (Init.Nat.add (S n) i) (S n)) vsl (@nil bool)) (@nth (list bool) i vsl (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  apply leb_complete in H1.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  replace (S n + i - S n) with i; trivial.
(* Goal: le sa s *)
  omega.
  
(* Goal: le s' s *)
  injection H1; clear H1; intros; subst.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  case_eq n; simpl; intros.
  destruct vsl; simpl; trivial.
(* Goal: @eq (list bool) (@cons bool b (if match n0 with | Datatypes.O => false | S m' => Nat.leb n0 m' end then @nth (list bool) (S n0) vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n0 n0) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  destruct n0.
  destruct vsl; simpl; trivial.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  case_eq (leb (S n0) n0); intros.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  apply leb_complete in H2.
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (S (S n0)) vnl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@cons bool b (@nth (list bool) (Init.Nat.sub (S n0) (S n0)) vsl (@nil bool))) (@cons bool b (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) (@tl bool (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool))) (@tl bool (@hd (list bool) (@nil bool) vsl)) *)
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  elimtype False; omega.
(* Goal: @eq (list bool) (@nth (list bool) (S (S (Init.Nat.sub (S n) (S n)))) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  rewrite minus_diag.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct vsl; trivial.

(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  destruct n.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  erewrite hd_nth_0; trivial.
(* Goal: @eq (list bool) (if Nat.leb (S (S (S (S n)))) n then @nth (list bool) (S (S (S (S (S (S (S (S n)))))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S (S n)))) (S n) with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  rewrite leb_correct_conv;[ | omega].
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  rewrite minus_diag; trivial.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  erewrite hd_nth_0; trivial.

(* Goal: le s' s *)
  injection H1; clear H1; intros; subst.
(* Goal: @eq (list bool) match (if match n with | Datatypes.O => false | S m' => Nat.leb n m' end then @nth (list bool) n vnl (@nil bool) else @nth (list bool) (Init.Nat.sub n n) vsl (@nil bool)) with | nil => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S m'0 as m') => Nat.leb n m'0 end then @nth (list bool) (S n) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S n | S l => Init.Nat.sub n l end vsl (@nil bool) | cons (true as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S n)) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S n) | S (Datatypes.O as l0) => S n | S (S l1 as l0) => Init.Nat.sub n l1 end vsl (@nil bool) | cons (false as b) l => if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else @nth (list bool) match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l0) => S (S n) | S (S (Datatypes.O as l1) as l0) => S n | S (S (S l2 as l1) as l0) => Init.Nat.sub n l2 end vsl (@nil bool) end match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  destruct n.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl.
  destruct vsl; simpl; trivial.
  destruct vsl; simpl; trivial.
  destruct l; simpl; trivial.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct b; trivial.
  destruct vsl; simpl; trivial.
  destruct l; simpl; trivial.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct b; trivial.
  destruct vsl; simpl; trivial.
(* Goal: @eq (list bool) (if Nat.leb (S (S (S (S n)))) n then @nth (list bool) (S (S (S (S (S (S (S (S n)))))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S (S n)))) (S n) with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  rewrite leb_correct_conv;[ | omega].
(* Goal: @eq (list bool) (@nth (list bool) (S (S (Init.Nat.sub (S n) (S n)))) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  rewrite minus_diag.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct vsl; trivial. 
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct n; trivial.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct n; trivial.
(* Goal: @eq (list bool) (if Nat.leb (S (S (S (S n)))) n then @nth (list bool) (S (S (S (S (S (S (S (S n)))))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S (S n)))) (S n) with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  rewrite leb_correct_conv;[ | omega].
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  rewrite <- minus_Sn_m; trivial.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl.
  destruct l; simpl; trivial.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct n; trivial.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct n; trivial.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: @eq (list bool) (if Nat.leb (S (S (S (S n)))) n then @nth (list bool) (S (S (S (S (S (S (S (S n)))))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S (S n)))) (S n) with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  rewrite leb_correct_conv;[ | omega].
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  rewrite <- minus_Sn_m; trivial.
(* Goal: @eq (list bool) (@nth (list bool) (S (S (Init.Nat.sub (S n) (S n)))) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  rewrite minus_diag.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: @eq (list bool) (if b then if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S m'1 as m'0) as m') => Nat.leb n m'1 end then @nth (list bool) (S (S (S n))) vnl (@nil bool) else match match n with | Datatypes.O => S (S n) | S (Datatypes.O as l) => S n | S (S l0 as l) => Init.Nat.sub n l0 end with | Datatypes.O => @cons bool b l | S m => @nth (list bool) m vsl (@nil bool) end else if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool b l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b0 (nil as l) => @nil bool | cons b0 (cons c (nil as l0) as l) => if b then c else @nil bool | cons b0 (cons c (cons d l1 as l0) as l) => if b then c else d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  destruct b.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct n; trivial.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct n; trivial.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct n; trivial.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: @eq (list bool) (if Nat.leb (S (S (S (S n)))) n then @nth (list bool) (S (S (S (S (S (S (S (S n)))))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S (S n)))) (S n) with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  rewrite leb_correct_conv;[ | omega].
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  rewrite <- minus_Sn_m; trivial.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  rewrite <- minus_Sn_m; trivial.
(* Goal: @eq (list bool) (@nth (list bool) (S (S (Init.Nat.sub (S n) (S n)))) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  rewrite minus_diag.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: le sa s *)
  omega.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct n; trivial.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct n; trivial.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct n; trivial.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct n; trivial.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: @eq (list bool) (if Nat.leb (S (S (S (S n)))) n then @nth (list bool) (S (S (S (S (S (S (S (S n)))))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S (S n)))) (S n) with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  rewrite leb_correct_conv;[ | omega].
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  rewrite <- minus_Sn_m; trivial.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  rewrite <- minus_Sn_m; trivial.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  rewrite <- minus_Sn_m; trivial.
(* Goal: @eq (list bool) (@nth (list bool) (S (S (Init.Nat.sub (S n) (S n)))) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  rewrite minus_diag.
(* Goal: @eq (list bool) (@nth (list bool) (S (S Datatypes.O)) vsl (@nil bool)) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: le (S n) (S (S n)) *)
(* Goal: le (S n) (S (S (S n))) *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  do 3 (destruct vsl; simpl; trivial).
(* Goal: le sa s *)
  omega.
(* Goal: le sa s *)
  omega.
 
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  case_eq (inf e1); intros; rewrite H2 in H1;[ | discriminate ].
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  case_eq (inf e2); intros; rewrite H3 in H1;[ | discriminate ].
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  case_eq (inf e3); intros; rewrite H4 in H1;[ | discriminate ].
(* Goal: le s' s *)
  injection H1; clear H1; intros; subst.  
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  apply maxl_le3 in H.
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  apply maxl_le3 in H0.
(* Goal: @eq (list bool) match Init.Nat.sub (S (S Datatypes.O)) Datatypes.O with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if Nat.leb (S (S (S n))) n then @nth (list bool) (S (S (S (S (S (S n)))))) vnl (@nil bool) else match Init.Nat.sub (S (S (S n))) (S n) with | Datatypes.O => @cons bool true l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => c | cons b (cons c (cons d l1 as l0) as l) => c end *)
(* Goal: @eq (list bool) (if match n with | Datatypes.O => false | S (Datatypes.O as m') => false | S (S (Datatypes.O as m'0) as m') => false | S (S (S (Datatypes.O as m'1) as m'0) as m') => false | S (S (S (S m'2 as m'1) as m'0) as m') => Nat.leb n m'2 end then @nth (list bool) (S (S (S (S n)))) vnl (@nil bool) else match match n with | Datatypes.O => S (S (S n)) | S (Datatypes.O as l) => S (S n) | S (S (Datatypes.O as l0) as l) => S n | S (S (S l1 as l0) as l) => Init.Nat.sub n l1 end with | Datatypes.O => @cons bool false l | S m => @nth (list bool) m vsl (@nil bool) end) match vsl with | nil => @nil bool | cons b (nil as l) => @nil bool | cons b (cons c (nil as l0) as l) => @nil bool | cons b (cons c (cons d l1 as l0) as l) => d end *)
(* Goal: @eq (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (semI e1) (semI e2) (semI e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  induction (hd nil vnl); simpl.
(* Goal: le sa s *)
  eapply IHe1; [ | | eauto ]; omega.
(* Goal: @eq (list bool) (if a then sem (conv n (S s) e3) (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) l (@tl (list bool) vnl) vsl) vsl) else sem (conv n (S s) e2) (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem (conv (Init.Nat.sub n (S Datatypes.O)) s e1)) (sem (conv n (S s) e2)) (sem (conv n (S s) e3)) l (@tl (list bool) vnl) vsl) vsl)) (if a then semI e3 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (semI e1) (semI e2) (semI e3) l (@tl (list bool) vnl) vsl) vsl) else semI e2 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (semI e1) (semI e2) (semI e3) l (@tl (list bool) vnl) vsl) vsl)) *)
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  case a; rewrite IHl.
(* Goal: le sa s *)
  eapply IHe3; [ | | eauto ]; omega.
(* Goal: le sa s *)
  eapply IHe2; [ | | eauto ]; omega.

(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  case_eq (inf e); intros; rewrite H4 in H3;[ | discriminate ].
  case_eq (leb n0 (length rl)); intros;
  case_eq (leb n1 (length tl)); intros;
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (I n n0) (E err')) (@In TypeI (E err') l)) *)
(* Goal: @ex ErrorI (fun err' : ErrorI => or (@eq TypeI (E e) (E err')) (@In TypeI (E err') l)) *)
  rewrite H5, H6 in H3; try discriminate.
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  simpl in H3.
  case_eq (inf_list (map inf rl)); intros;
    rewrite H7 in H3; [ | discriminate ].
  case_eq (inf_list (map inf tl)); intros;
    rewrite H8 in H3; [ | discriminate ].
  case_eq (beq_nat n3 0); intros; 
    rewrite H9 in H3; [ | discriminate ].
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  apply leb_complete in H5.
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  apply leb_complete in H6.
(* Goal: @eq (list bool) (sem (conv (@length BCI rl) (@length BCI tl) e) (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  apply beq_nat_true in H9.  
(* Goal: le sa s *)
  erewrite IHe; [ | | | eauto]; try omega.
(* Goal: @eq (list bool) (semI e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  clear IHe.
(* Goal: le s' s *)
  injection H3; clear H3; intros; subst. 
(* Goal: @eq (list bool) (semI e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) (@map BCI BC (conv n Datatypes.O) rl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl))) (semI e (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) rl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl)) *)
  f_equal.
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  rewrite map_map.
(* Goal: @eq (list (list bool)) (@map BCI (list bool) (fun x : BCI => sem (conv n s x) vnl vsl) tl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  apply map_ext2.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  intros.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  eapply (inf_list_ex _ a) in H7; trivial.
(* Goal: @eq (list bool) (sem (conv n Datatypes.O a) vnl (@nil (list bool))) (semI a vnl (@nil (list bool))) *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  destruct H7 as (na & sa & Ha1 & Ha2 & Ha3).
  eapply H;[ trivial | |  | apply Ha3 ].
(* Goal: le na n *)
(* Goal: le sa s *)
  apply le_trans with (2 := H1).
(* Goal: le na (Init.Nat.max n2 n4) *)
(* Goal: le sa s *)
  apply le_trans with (1 := Ha1).
(* Goal: le n4 (Init.Nat.max n2 n4) *)
(* Goal: le sa s *)
  auto with arith.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  trivial.
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  rewrite map_map.
(* Goal: @eq (list (list bool)) (@map BCI (list bool) (fun x : BCI => sem (conv n s x) vnl vsl) tl) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  apply map_ext2.
(* Goal: forall (a : BCI) (_ : @In BCI a tl), @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  intros.
(* Goal: le sa Datatypes.O *)
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) (@map BCI BC (conv n s) tl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) tl) *)
  eapply (inf_list_ex _ a) in H8; trivial.
(* Goal: @eq (list bool) (sem (conv n s a) vnl vsl) (semI a vnl vsl) *)
  destruct H8 as (na & sa & Ha1 & Ha2 & Ha3).
  eapply H0;[ trivial | |  | apply Ha3 ].
(* Goal: le na n *)
(* Goal: le sa s *)
  apply le_trans with (2 := H1).
(* Goal: le na (Init.Nat.max n2 n4) *)
(* Goal: le sa s *)
  apply le_trans with (1 := Ha1).
(* Goal: le n4 (Init.Nat.max n2 n4) *)
(* Goal: le sa s *)
  auto with arith.
(* Goal: le sa s *)
  omega.
Qed.

Definition conv_bci_to_bc (e : BCI) : option BC :=
  match inf e with
  | I n s => Some (conv n s e)
  | _ => None
end.

Lemma conv_bci_to_bc_correct : forall (e : BCI) (e' : BC) (vnl vsl : list bs),
  conv_bci_to_bc e = Some e' ->
  sem e' vnl vsl = semI e vnl vsl.
Proof.
(* Goal: forall (e : BCI) (e' : BC) (vnl vsl : list (list bool)) (_ : @eq (option BC) (conv_bci_to_bc e) (@Some BC e')), @eq (list bool) (sem e' vnl vsl) (semI e vnl vsl) *)
 unfold conv_bci_to_bc; intros e e' vnl vsl.
(* Goal: forall _ : @eq (option BC) match inf e with | I n s => @Some BC (conv n s e) | E e => @None BC end (@Some BC e'), @eq (list bool) (sem e' vnl vsl) (semI e vnl vsl) *)
 case_eq (inf e);[ | discriminate ].
(* Goal: forall (n n0 : nat) (_ : @eq TypeI (inf e) (I n n0)) (_ : @eq (option BC) (@Some BC (conv n n0 e)) (@Some BC e')), @eq (list bool) (sem e' vnl vsl) (semI e vnl vsl) *)
 intros n s Hinf H.
(* Goal: @eq (list bool) (sem e' vnl vsl) (semI e vnl vsl) *)
 injection H; clear H; intro H.
(* Goal: @eq (list bool) (sem e' vnl vsl) (semI e vnl vsl) *)
 rewrite <- H.
(* Goal: @eq (list bool) (sem (conv n s e) vnl vsl) (semI e vnl vsl) *)
 apply conv_correct with n s; auto.
Qed.



