Require Import Bool Arith List.
Require Import BellantoniCook.Lib BellantoniCook.MultiPoly BellantoniCook.Cobham BellantoniCook.CobhamLib BellantoniCook.CobhamUnary BellantoniCook.BC.

Definition Pred : Cobham :=
  Rec Zero (Proj 2 0) (Proj 2 0) (Proj 1 0).

(* Eval vm_compute in (arity pred'). *)

Lemma rec_bounded_Pred : rec_bounded' Pred.
Proof.
(* Goal: rec_bounded' Pred *)
  simpl; repeat (split; auto); intros.
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (@nth (list bool) O l (@nil bool))) *)
  rewrite <- hd_nth_0.
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (@hd (list bool) (@nil bool) l)) *)
  induction (hd nil l); simpl; try (case a); omega.
Qed.

Lemma Pred_correct l :
  sem pred nil l = Sem Pred l.
Proof.
(* Goal: @eq (list bool) (sem cond (@nil (list bool)) l) (Sem Cond l) *)
  intros; simpl.
(* Goal: @eq (list bool) (@tl bool (@hd (list bool) (@nil bool) l)) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) *)
  case (hd nil l); simpl; trivial.
(* Goal: forall (b : bool) (l : list bool), @eq (list bool) l (if b then l else l) *)
  intros; case b; trivial.
Qed.

Lemma cond'_correct l :
  sem cond nil l = Sem Cond l.
Proof.
(* Goal: @eq (list bool) (sem cond (@nil (list bool)) l) (Sem Cond l) *)
  intros; simpl.
(* Goal: @eq (list bool) match l0 with | nil => @nil bool | cons b (nil as l0) => match l with | nil => b | cons b0 l => @nil bool end | cons b (cons c (nil as l1) as l0) => match l with | nil => b | cons (true as b0) l => c | cons (false as b0) l => @nil bool end | cons b (cons c (cons d l2 as l1) as l0) => match l with | nil => b | cons (true as b0) l => c | cons (false as b0) l => d end end (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) l l0) *)
  destruct l; simpl; trivial; intros.
(* Goal: @eq (list bool) match l0 with | nil => @nil bool | cons b (nil as l0) => match l with | nil => b | cons b0 l => @nil bool end | cons b (cons c (nil as l1) as l0) => match l with | nil => b | cons (true as b0) l => c | cons (false as b0) l => @nil bool end | cons b (cons c (cons d l2 as l1) as l0) => match l with | nil => b | cons (true as b0) l => c | cons (false as b0) l => d end end (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) l l0) *)
  destruct l; simpl; trivial; intros.
(* Goal: @eq (list bool) match l0 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 (if b then @nth (list bool) (S O) l0 (@nil bool) else @nth (list bool) (S (S O)) l0 (@nil bool)) *)
  destruct l0; simpl; trivial; intros.
(* Goal: @eq (list bool) match l0 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 (if b then @nth (list bool) (S O) l0 (@nil bool) else @nth (list bool) (S (S O)) l0 (@nil bool)) *)
  destruct l0; simpl; trivial; intros.
(* Goal: @eq (list bool) match l1 with | nil => @nil bool | cons c (nil as l) => if b then c else @nil bool | cons c (cons d l0 as l) => if b then c else d end (if b then @nth (list bool) O l1 (@nil bool) else @nth (list bool) (S O) l1 (@nil bool)) *)
  destruct l1; simpl; trivial; intros.
(* Goal: @eq (list bool) match l0 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 (if b then @nth (list bool) (S O) l0 (@nil bool) else @nth (list bool) (S (S O)) l0 (@nil bool)) *)
  destruct l0; simpl; trivial; intros.
(* Goal: @eq (list bool) (@nil bool) (if b then @nil bool else @nil bool) *)
(* Goal: @eq (list bool) match l2 with | nil => if b then l1 else @nil bool | cons d l => if b then l1 else d end (if b then l1 else @nth (list bool) O l2 (@nil bool)) *)
  destruct b; simpl; trivial; intros.
(* Goal: @eq (list bool) match l1 with | nil => @nil bool | cons c (nil as l) => if b then c else @nil bool | cons c (cons d l0 as l) => if b then c else d end (if b then @nth (list bool) O l1 (@nil bool) else @nth (list bool) (S O) l1 (@nil bool)) *)
  destruct l1; simpl; trivial; intros.
(* Goal: @eq (list bool) (@nil bool) (if b then @nil bool else @nil bool) *)
(* Goal: @eq (list bool) match l2 with | nil => if b then l1 else @nil bool | cons d l => if b then l1 else d end (if b then l1 else @nth (list bool) O l2 (@nil bool)) *)
  destruct b; simpl; trivial; intros.
(* Goal: @eq (list bool) match l2 with | nil => if b then l1 else @nil bool | cons d l => if b then l1 else d end (if b then l1 else @nth (list bool) O l2 (@nil bool)) *)
  destruct l2; simpl; trivial; intros.
Qed.

Definition move_arg (n i j:nat) (e:Cobham) : Cobham :=
  Comp n e (move_forward i j 
    (map (Proj n) (seq 0 n)) (Proj n 0)).

Lemma move_arg_inf n i j e :
  i+j < n -> arity e = ok_arity n ->
  arity (move_arg n i j e) = ok_arity n.
Proof.
(* Goal: forall _ : @eq nat (@length (list bool) l) n, @eq (list bool) (Sem (move_arg n i j e) l) (Sem e (@move_forward (list bool) i j l (Sem (Proj n O) l))) *)
  simpl; intros.
(* Goal: @eq Arity match arity e with | error_Rec a a0 a1 a2 => error_Comp (error_Rec a a0 a1 a2) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O))) | error_Comp a l => error_Comp (error_Comp a l) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O))) | error_Proj n0 n1 => error_Comp (error_Proj n0 n1) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O))) | ok_arity nh => if andb (Nat.eqb nh (@length Cobham (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (@forallb Arity (fun e : Arity => arity_eq e (ok_arity n)) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) then ok_arity n else error_Comp (ok_arity nh) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O))) end (ok_arity n) *)
  rewrite H0, length_move_forward, map_length, seq_length, <- beq_nat_refl; simpl.
  case_eq (forallb (fun e0 : Arity => arity_eq e0 (ok_arity n))
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
      (map arity (move_forward i j (map (Proj n) (seq 0 n)) (Proj n 0)))); trivial.
(* Goal: forall _ : @eq bool (@forallb Arity (fun e0 : Arity => arity_eq e0 (ok_arity n)) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) false, @eq Arity (error_Comp (ok_arity n) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (ok_arity n) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  intros Hall.
(* Goal: @eq Arity (error_Comp (ok_arity n) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (ok_arity n) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite forallb_forall_conv in Hall.
(* Goal: @eq Arity (error_Comp (ok_arity n) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (ok_arity n) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  destruct Hall as [n' [H1 H2] ].
(* Goal: @eq Arity (error_Comp (ok_arity n) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (ok_arity n) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite in_map_iff in H1.
(* Goal: @eq Arity (error_Comp (ok_arity n) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (ok_arity n) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  destruct H1 as [e' [H3 H4] ].
(* Goal: @eq Arity (error_Comp (ok_arity n) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (ok_arity n) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite move_forward_map with (d1:=0) in H4 by trivial.
(* Goal: @eq Arity (error_Comp (ok_arity n) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (ok_arity n) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite in_map_iff in H4.
(* Goal: @eq Arity (error_Comp (ok_arity n) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (ok_arity n) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  destruct H4 as [n'' [H5 H6] ]; subst.
(* Goal: @eq Arity (error_Comp (ok_arity n) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (ok_arity n) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite in_move_forward_iff in H6.
(* Goal: @eq Arity (error_Comp (ok_arity n) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (ok_arity n) *)
(* Goal: lt i (@length nat (seq O n)) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite in_seq_iff in H6.
(* Goal: @eq Arity (error_Comp (ok_arity n) (@map Cobham Arity arity (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O)))) (ok_arity n) *)
(* Goal: lt i (@length nat (seq O n)) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  replace (arity (Proj n n'')) with (ok_arity n) in H2.
(* Goal: @eq Arity (ok_arity O) (error_Proj O n'') *)
(* Goal: @eq Arity (ok_arity (S n)) (if Nat.leb n'' n then ok_arity (S n) else error_Proj (S n) n'') *)
(* Goal: lt i (@length nat (seq O n)) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  contradict H2.
(* Goal: not (@eq bool (arity_eq (ok_arity n) (ok_arity n)) false) *)
(* Goal: @eq Arity (ok_arity n) (arity (Proj n n'')) *)
(* Goal: lt i (@length nat (seq O n)) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite arity_eq_refl.
(* Goal: not (@eq bool true false) *)
(* Goal: @eq Arity (ok_arity n) (arity (Proj n n'')) *)
(* Goal: lt i (@length nat (seq O n)) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  congruence.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  simpl.
(* Goal: @eq (list bool) (if match n with | O => false | S m' => Nat.leb i m' end then @nth (list bool) i xl (@nil bool) else @nth (list bool) (Init.Nat.sub i n) yl (@nil bool)) (@nth (list bool) i (@app (list bool) xl yl) (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (@hd (list bool) (@nil bool) yl)) (@cons bool b (@hd (list bool) (@nil bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (@tl bool (@hd (list bool) (@nil bool) yl)) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) match yl 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 (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham (Init.Nat.sub n O) s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  destruct n.
(* Goal: @eq Arity (ok_arity O) (error_Proj O n'') *)
(* Goal: @eq Arity (ok_arity (S n)) (if Nat.leb n'' n then ok_arity (S n) else error_Proj (S n) n'') *)
(* Goal: lt i (@length nat (seq O n)) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  contradict H2.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  omega.
(* Goal: @eq Arity (ok_arity (S n)) (if Nat.leb n'' n then ok_arity (S n) else error_Proj (S n) n'') *)
(* Goal: lt i (@length nat (seq O n)) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite leb_correct by omega; trivial.
(* Goal: lt i (@length nat (seq O n)) *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite seq_length.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  omega.
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite map_length, seq_length; trivial.
Qed.

Lemma rec_bounded_move_arg : forall n i j e,
  rec_bounded' e ->
  rec_bounded' (move_arg n i j e).
Proof.
(* Goal: forall (n i j : nat) (e : Cobham) (_ : rec_bounded' e), rec_bounded' (move_arg n i j e) *)
  intros n i j e H; simpl; split; trivial.
(* Goal: @andl Cobham rec_bounded' (@map nat Cobham (Proj (Init.Nat.add n m)) (seq O n)) *)
  rewrite <- forall_andl.
(* Goal: forall (x : Cobham) (_ : @In Cobham x (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O))), rec_bounded' x *)
  intros e' H'.
(* Goal: rec_bounded' e' *)
  rewrite move_forward_map with (d1:=0), in_map_iff in H' by trivial.
(* Goal: rec_bounded' e' *)
  destruct H' as [m [H1 _] ]; subst; simpl; trivial.
Qed.

Lemma move_arg_correct n i j e l :
  length l = n ->
  Sem (move_arg n i j e) l = 
  Sem e (move_forward i j l (Sem (Proj n 0) l)).
Proof.
(* Goal: forall _ : @eq nat (@length (list bool) l) n, @eq (list bool) (Sem (move_arg n i j e) l) (Sem e (@move_forward (list bool) i j l (Sem (Proj n O) l))) *)
  simpl; intros.
(* Goal: @eq (list bool) (Sem e (@map nat (list bool) (fun x : nat => @nth (list bool) x l (@nil bool)) (seq O n))) (Sem e (@firstn (list bool) n l)) *)
  f_equal.
(* Goal: @eq (list (list bool)) (@map Cobham (list bool) (fun e : Cobham => Sem e l) (@move_forward Cobham i j (@map nat Cobham (Proj n) (seq O n)) (Proj n O))) (@move_forward (list bool) i j l (@nth (list bool) O l (@nil bool))) *)
  rewrite <- move_forward_map with (d2:= Sem (Proj n 0) l); trivial.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite map_map; simpl.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  f_equal; apply map_nth_seq; omega.
Qed.

Definition dummies (n m : nat)(e : Cobham) : Cobham :=
  Comp (n+m) e (map (Proj (n+m)) (seq 0 n)).

Lemma arity_dummies e n n' :
  arity e = ok_arity n' ->
  arity (dummies n' n e) = ok_arity (n + n').
Proof.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
destruct n' as [ | n']; intro H; simpl; rewrite H; simpl.
(* Goal: @eq Arity (ok_arity n) (ok_arity (Init.Nat.add n O)) *)
(* Goal: @eq Arity (if andb (Nat.eqb n' (@length Cobham (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n')))) (andb (Nat.eqb (Init.Nat.add n' n) (Init.Nat.add n' n)) (@forallb Arity (fun e : Arity => arity_eq e (ok_arity (S (Init.Nat.add n' n)))) (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n'))))) then ok_arity (S (Init.Nat.add n' n)) else error_Comp (ok_arity (S n')) (@cons Arity (ok_arity (S (Init.Nat.add n' n))) (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n'))))) (ok_arity (Init.Nat.add n (S n'))) *)
rewrite plus_0_r.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
trivial.
(* Goal: @eq Arity (if andb (Nat.eqb n' (@length Cobham (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n')))) (andb (Nat.eqb (Init.Nat.add n' n) (Init.Nat.add n' n)) (@forallb Arity (fun e : Arity => arity_eq e (ok_arity (S (Init.Nat.add n' n)))) (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n'))))) then ok_arity (S (Init.Nat.add n' n)) else error_Comp (ok_arity (S n')) (@cons Arity (ok_arity (S (Init.Nat.add n' n))) (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n'))))) (ok_arity (Init.Nat.add n (S n'))) *)
rewrite map_length, seq_length, <- beq_nat_refl, <- beq_nat_refl.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
simpl.
case_eq (forallb (fun e0 : Arity => arity_eq e0 (ok_arity (S (n' + n))))
      (map arity (map (Proj (S (n' + n))) (seq 1 n')))); intro Hall.
(* Goal: @eq (list bool) (Sem e (@map nat (list bool) (fun x : nat => @nth (list bool) x l (@nil bool)) (seq O n))) (Sem e (@firstn (list bool) n l)) *)
f_equal.
(* Goal: @eq nat (S (Init.Nat.add n' n)) (Init.Nat.add n (S n')) *)
(* Goal: @eq Arity (error_Comp (ok_arity (S n')) (@cons Arity (ok_arity (S (Init.Nat.add n' n))) (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n'))))) (ok_arity (Init.Nat.add n (S n'))) *)
ring.
(* Goal: @eq Arity (error_Comp (ok_arity (S n')) (@cons Arity (ok_arity (S (Init.Nat.add n' n))) (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n'))))) (ok_arity (Init.Nat.add n (S n'))) *)
rewrite <- not_true_iff_false in Hall.
(* Goal: @eq Arity (error_Comp (ok_arity (S n')) (@cons Arity (ok_arity (S (Init.Nat.add n' n))) (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n'))))) (ok_arity (Init.Nat.add n (S n'))) *)
contradict Hall.
(* Goal: @eq bool (@forallb Arity (fun e0 : Arity => arity_eq e0 (ok_arity (S (Init.Nat.add n' n)))) (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n')))) true *)
rewrite forallb_forall.
(* Goal: forall (x : Arity) (_ : @In Arity x (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n')))), @eq bool (arity_eq x (ok_arity (S (Init.Nat.add n' n)))) true *)
intros m H0.
(* Goal: rec_bounded' e0 *)
rewrite in_map_iff in H0.
(* Goal: @eq bool (arity_eq m (ok_arity (S (Init.Nat.add n' n)))) true *)
destruct H0 as [e0 [H1 H2] ].
(* Goal: @eq bool (arity_eq m (ok_arity (S (Init.Nat.add n' n)))) true *)
rewrite in_map_iff in H2.
(* Goal: @eq bool (arity_eq m (ok_arity (S (Init.Nat.add n' n)))) true *)
destruct H2 as [p [H3 H4] ].
(* Goal: @eq bool (arity_eq m (ok_arity (S (Init.Nat.add n' n)))) true *)
rewrite in_seq_iff in H4.
(* Goal: @eq bool (arity_eq m (ok_arity (S (Init.Nat.add n' n)))) true *)
subst e0 m.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
simpl.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
rewrite leb_correct by omega.
(* Goal: @eq bool (arity_eq (ok_arity (S (Init.Nat.add n' n))) (ok_arity (S (Init.Nat.add n' n)))) true *)
apply arity_eq_refl.
Qed.

Lemma rec_bounded_dummies : forall e n m,
  rec_bounded' e ->
  rec_bounded' (dummies n m e). 
Proof.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
intros e n m H; simpl; split; trivial.
(* Goal: @andl Cobham rec_bounded' (@map nat Cobham (Proj (Init.Nat.add n m)) (seq O n)) *)
rewrite <- forall_andl.
(* Goal: forall (x : Cobham) (_ : @In Cobham x (@map nat Cobham (Proj (Init.Nat.add n m)) (seq O n))), rec_bounded' x *)
intros e0 H0.
(* Goal: rec_bounded' e0 *)
rewrite in_map_iff in H0.
(* Goal: rec_bounded' e0 *)
destruct H0 as [p [H1 _] ].
(* Goal: rec_bounded' e0 *)
subst e0.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
simpl; trivial.
Qed.

Lemma dummies_correct e n m l:
  n <= length l ->
  Sem (dummies n m e) l = Sem e (firstn n l). 
Proof.
(* Goal: @eq (list bool) (sem cond (@nil (list bool)) l) (Sem Cond l) *)
unfold dummies; intros; simpl.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
rewrite map_map; simpl.
(* Goal: @eq (list bool) (Sem e (@map nat (list bool) (fun x : nat => @nth (list bool) x l (@nil bool)) (seq O n))) (Sem e (@firstn (list bool) n l)) *)
f_equal.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
rewrite <- firstn_map_nth; trivial.
Qed.

(* n s : arities of e*)
Fixpoint BC_to_Cobham n s (e : BC) : Cobham :=
  match e with
    | zero => Zero
    | proj n s i => Proj (n + s) i
    | succ b => Succ b
    | pred => Pred
    | cond => Cond
    | rec g h0 h1 =>
        Rec (BC_to_Cobham (n - 1) s g)
        (move_arg (S (n+s)) 1 (n-1) (BC_to_Cobham n (S s) h0) )
        (move_arg (S (n+s)) 1 (n-1) (BC_to_Cobham n (S s) h1) )
        (Poly (pplus (psum n s) (poly_BC n e)))
    | comp n s h rl tl =>
      Comp (n + s) (BC_to_Cobham (length rl) (length tl) h)
      (map (fun e => (dummies n s (BC_to_Cobham n 0 e))) rl ++ 
        map (BC_to_Cobham n s) tl)
  end.

Opaque Poly.

Lemma arity_BC_to_Cobham : forall (e : BC) n s,
  arities e = ok_arities n s ->
  arity (BC_to_Cobham n s e) = ok_arity (n + s).
Proof.
(* Goal: forall (e : BC) (n s : nat) (_ : @eq Arities (arities e) (ok_arities n s)) (xl yl : list (list bool)) (_ : @eq nat n (@length (list bool) xl)) (_ : @eq nat s (@length (list bool) yl)), @eq (list bool) (sem e xl yl) (Sem (BC_to_Cobham n s e) (@app (list bool) xl yl)) *)
  refine (BC_ind_inf _ _ _ _ _ _ _ _ ); simpl; intros; auto.
  destruct (n + s).
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  contradict H; omega.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  case_eq (leb i n0); intros; trivial.
  apply leb_complete_conv in H0.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  contradict H0; omega.
  Opaque move_arg.
  Opaque psum.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite <- minus_n_O, H2, H3, H4; auto; simpl.
  cutrewrite (length
    (firstn n (map (Proj (S (S (n + s)))) (seq 2 (n + s))) ++
      Proj (S (S (n + s))) 1
      :: skipn n (map (Proj (S (S (n + s)))) (seq 2 (n + s)))) = n + S s).
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  repeat rewrite <- beq_nat_refl; simpl.
  case_eq (forallb (fun e : Arity => arity_eq e (ok_arity (S (S (n + s)))))
           (map arity
              (firstn n (map (Proj (S (S (n + s)))) (seq 2 (n + s))) ++
               Proj (S (S (n + s))) 1
(* Goal: @eq (list bool) (sem cond (@nil (list bool)) l) (Sem Cond l) *)
               :: skipn n (map (Proj (S (S (n + s)))) (seq 2 (n + s)))))); intros; simpl.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite arity_Poly, <- beq_nat_refl; simpl.
  rewrite parity_psum.
  erewrite arity_poly_BC; eauto.
  erewrite arity_poly_BC; eauto.
  erewrite arity_poly_BC; eauto.
  repeat rewrite Nat.max_idempotent.
  rewrite max_l; [ | omega].
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite <- beq_nat_refl; simpl; trivial.
  pWF; eapply pWF_poly_BC; eauto.

  elimtype False.
  apply eq_true_false_abs in H5; trivial; clear H5.
  apply forallb_forall; intros.
  apply in_map_iff in H5.
  destruct H5 as (? & ? & ?); subst.
  apply in_app_or in H6; destruct H6.
  rewrite <- map_firstn in H5.
  apply in_map_iff in H5.
  destruct H5 as (? & ? & ?); subst.
  rewrite firstn_seq in H6.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  apply in_seq_iff in H6; simpl.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite leb_correct; simpl.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite <- beq_nat_refl; trivial.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite Min.min_l in H6; omega.
  simpl in H5.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  destruct H5; subst; simpl.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite <- beq_nat_refl; trivial.
  rewrite <- map_skipn in H5.
  apply in_map_iff in H5.
  destruct H5 as (? & ? & ?); subst.
  rewrite skipn_seq in H6.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  apply in_seq_iff in H6; simpl.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite leb_correct; simpl.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite <- beq_nat_refl; trivial.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  omega.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite app_length, firstn_length, map_length, seq_length; simpl.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite skipn_length, map_length, seq_length; simpl.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite Min.min_l; omega.
  
  rewrite H2.
  rewrite app_length.
  repeat rewrite map_length.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite <- beq_nat_refl; simpl.
  case_eq ( forallb 
    (fun e : Arity => arity_eq e (ok_arity (n + s)))
    (map arity
      (map (fun e : BC => dummies n s (BC_to_Cobham n 0 e)) rl ++
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
        map (BC_to_Cobham n s) tl))); intros; trivial.
  elimtype False.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  apply eq_true_false_abs in H5; trivial.
  eapply forallb_forall; intros.
  apply in_map_iff in H6.
  destruct H6 as [c [Hc1 Hc2]].
  apply in_app_or in Hc2.
  destruct Hc2.

  subst.
  apply in_map_iff in H6.
  destruct H6 as [bc [Hbc1 Hbc2]].
  subst.
  erewrite arity_dummies.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  simpl.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite plus_comm, <- beq_nat_refl; trivial.
  rewrite (plus_n_O n) at 2.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  apply H3; trivial.
  apply in_map_iff in H6.
  destruct H6 as [bc [Hbc1 Hbc2]].
  subst.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite H4; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  simpl; rewrite <- beq_nat_refl; trivial.
Qed.

Lemma BC_to_Cobham_correct : forall (e : BC) n s,
  arities e = ok_arities n s ->
  (forall xl yl,
  n = length xl ->
  s = length yl ->
  sem e xl yl = Sem (BC_to_Cobham n s e) (xl ++ yl)).
Proof.
(* Goal: forall (e : BC) (n s : nat) (_ : @eq Arities (arities e) (ok_arities n s)) (xl yl : list (list bool)) (_ : @eq nat n (@length (list bool) xl)) (_ : @eq nat s (@length (list bool) yl)), @eq (list bool) (sem e xl yl) (Sem (BC_to_Cobham n s e) (@app (list bool) xl yl)) *)
  refine (BC_ind_inf _ _ _ _ _ _ _ _); simpl; intros; auto.
(* Goal: @eq (list bool) (if match n with | O => false | S m' => Nat.leb i m' end then @nth (list bool) i xl (@nil bool) else @nth (list bool) (Init.Nat.sub i n) yl (@nil bool)) (@nth (list bool) i (@app (list bool) xl yl) (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (@hd (list bool) (@nil bool) yl)) (@cons bool b (@hd (list bool) (@nil bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (@tl bool (@hd (list bool) (@nil bool) yl)) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) match yl 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 (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham (Init.Nat.sub n O) s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  destruct n.
(* Goal: @eq (list bool) match yl 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 (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham (Init.Nat.sub n O) s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  rewrite (length_nil _ xl); simpl; auto.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  f_equal; omega.
(* Goal: @eq (list bool) (if Nat.leb i n then @nth (list bool) i xl (@nil bool) else @nth (list bool) (Init.Nat.sub i (S n)) yl (@nil bool)) (@nth (list bool) i (@app (list bool) xl yl) (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (@hd (list bool) (@nil bool) yl)) (@cons bool b (@hd (list bool) (@nil bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (@tl bool (@hd (list bool) (@nil bool) yl)) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) match yl 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 (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham (Init.Nat.sub n O) s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  case_eq (leb i n); intros.
(* Goal: @eq (list bool) (@nth (list bool) i xl (@nil bool)) (@nth (list bool) i (@app (list bool) xl yl) (@nil bool)) *)
(* Goal: @eq (list bool) (@nth (list bool) (Init.Nat.sub i (S n)) yl (@nil bool)) (@nth (list bool) i (@app (list bool) xl yl) (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (@hd (list bool) (@nil bool) yl)) (@cons bool b (@hd (list bool) (@nil bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (@tl bool (@hd (list bool) (@nil bool) yl)) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) match yl 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 (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham (Init.Nat.sub n O) s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  apply leb_complete in H2.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite app_nth1; trivial; omega.
(* Goal: @eq (list bool) (@nth (list bool) (Init.Nat.sub i (S n)) yl (@nil bool)) (@nth (list bool) i (@app (list bool) xl yl) (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (@hd (list bool) (@nil bool) yl)) (@cons bool b (@hd (list bool) (@nil bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (@tl bool (@hd (list bool) (@nil bool) yl)) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) match yl 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 (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham (Init.Nat.sub n O) s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  apply leb_complete_conv in H2.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite app_nth2, H0; trivial; omega.
(* Goal: @eq (list bool) match yl 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 (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham (Init.Nat.sub n O) s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  rewrite (length_nil _ xl); simpl; auto.
(* Goal: @eq (list bool) match yl 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 (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham (Init.Nat.sub n O) s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  rewrite (length_nil _ xl); simpl; auto.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  destruct (hd nil yl); simpl; trivial; case b; trivial.
(* Goal: @eq (list bool) match yl 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 (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham (Init.Nat.sub n O) s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  rewrite (length_nil _ xl); simpl; auto.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  destruct yl; simpl; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  destruct yl; simpl; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  destruct l; simpl; trivial; case b; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  destruct yl; simpl; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  destruct l; simpl; trivial; case b; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  destruct yl; simpl; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  destruct l; simpl; trivial; case b; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  destruct l; simpl; trivial; case b; trivial.
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham (Init.Nat.sub n O) s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  rewrite <- minus_n_O.
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  destruct xl; simpl in *.
(* Goal: @eq (list bool) (sem g (@nil (list bool)) yl) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) yl) (@tl (list bool) yl)) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) l (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  discriminate.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  induction l; simpl.
(* Goal: @eq (list bool) (sem g xl yl) (Sem (BC_to_Cobham n s g) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (if a then sem h1 (@cons (list bool) l xl) (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) yl) else sem h0 (@cons (list bool) l xl) (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) yl)) (if a then Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1)) (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) l (@app (list bool) xl yl)) (@app (list bool) xl yl))) else Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0)) (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) l (@app (list bool) xl yl)) (@app (list bool) xl yl)))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  apply H2; auto.
(* Goal: @eq (list bool) (if a then sem h1 (@cons (list bool) l xl) (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) yl) else sem h0 (@cons (list bool) l xl) (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) yl)) (if a then Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1)) (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) l (@app (list bool) xl yl)) (@app (list bool) xl yl))) else Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0)) (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) l (@app (list bool) xl yl)) (@app (list bool) xl yl)))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  rewrite <- IHl.
(* Goal: @eq (list bool) (if a then sem h1 (@cons (list bool) l xl) (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) yl) else sem h0 (@cons (list bool) l xl) (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) yl)) (if a then Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1)) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl))) else Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0)) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl)))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  rewrite H3, H4; simpl; auto.  
  injection H5; intros; subst.
(* Goal: @eq (list bool) (if a then Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h1) (@cons (list bool) l (@app (list bool) xl (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) yl))) else Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h0) (@cons (list bool) l (@app (list bool) xl (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) yl)))) (if a then Sem (move_arg (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) (S O) (@length (list bool) xl) (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h1)) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl))) else Sem (move_arg (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) (S O) (@length (list bool) xl) (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h0)) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl)))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  repeat rewrite move_arg_correct.
(* Goal: @eq (list bool) (if a then Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h1) (@cons (list bool) l (@app (list bool) xl (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) yl))) else Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h0) (@cons (list bool) l (@app (list bool) xl (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) yl)))) (if a then Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h1) (@move_forward (list bool) (S O) (@length (list bool) xl) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl))) (Sem (Proj (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) O) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl))))) else Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h0) (@move_forward (list bool) (S O) (@length (list bool) xl) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl))) (Sem (Proj (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) O) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl)))))) *)
(* Goal: @eq nat (@length (list bool) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl)))) (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) *)
(* Goal: @eq nat (@length (list bool) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl)))) (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  set (r := sem_rec (sem g) (sem h0) (sem h1) l xl yl).
(* Goal: @eq (list bool) (if a then Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h1) (@cons (list bool) l (@app (list bool) xl (@cons (list bool) r yl))) else Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h0) (@cons (list bool) l (@app (list bool) xl (@cons (list bool) r yl)))) (if a then Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h1) (@move_forward (list bool) (S O) (@length (list bool) xl) (@cons (list bool) l (@cons (list bool) r (@app (list bool) xl yl))) (Sem (Proj (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) O) (@cons (list bool) l (@cons (list bool) r (@app (list bool) xl yl))))) else Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h0) (@move_forward (list bool) (S O) (@length (list bool) xl) (@cons (list bool) l (@cons (list bool) r (@app (list bool) xl yl))) (Sem (Proj (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) O) (@cons (list bool) l (@cons (list bool) r (@app (list bool) xl yl)))))) *)
(* Goal: @eq nat (@length (list bool) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl)))) (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) *)
(* Goal: @eq nat (@length (list bool) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl)))) (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  assert (l :: xl ++ r :: yl = move_forward 1 (length xl) (l :: r :: xl ++ yl) l) as Hmf.
(* Goal: @eq (list bool) (Sem e (@map nat (list bool) (fun x : nat => @nth (list bool) x l (@nil bool)) (seq O n))) (Sem e (@firstn (list bool) n l)) *)
  unfold move_forward; simpl; f_equal.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite firstn_app, skipn_app; trivial.
(* Goal: @eq (list bool) (if a then Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h1) (@cons (list bool) l (@app (list bool) xl (@cons (list bool) r yl))) else Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h0) (@cons (list bool) l (@app (list bool) xl (@cons (list bool) r yl)))) (if a then Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h1) (@move_forward (list bool) (S O) (@length (list bool) xl) (@cons (list bool) l (@cons (list bool) r (@app (list bool) xl yl))) (Sem (Proj (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) O) (@cons (list bool) l (@cons (list bool) r (@app (list bool) xl yl))))) else Sem (BC_to_Cobham (S (@length (list bool) xl)) (S (@length (list bool) yl)) h0) (@move_forward (list bool) (S O) (@length (list bool) xl) (@cons (list bool) l (@cons (list bool) r (@app (list bool) xl yl))) (Sem (Proj (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) O) (@cons (list bool) l (@cons (list bool) r (@app (list bool) xl yl)))))) *)
(* Goal: @eq nat (@length (list bool) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl)))) (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) *)
(* Goal: @eq nat (@length (list bool) (@cons (list bool) l (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (@app (list bool) xl yl)))) (S (S (Init.Nat.add (@length (list bool) xl) (@length (list bool) yl)))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  rewrite Hmf.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  case a; f_equal; simpl.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  simpl; rewrite app_length; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  simpl; rewrite app_length; trivial.
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  rewrite map_app.
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl)) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  do 2 rewrite map_map.
  assert (HA : map (fun ne : BC => sem ne xl nil) rl = 
    map (fun x : BC => Sem (dummies (length xl) (length yl) 
      (BC_to_Cobham (length xl) 0 x)) (xl ++ yl)) rl).
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun x : BC => Sem (dummies (@length (list bool) xl) (@length (list bool) yl) (BC_to_Cobham (@length (list bool) xl) O x)) (@app (list bool) xl yl)) rl) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  apply map_ext2.
(* Goal: forall (a : BC) (_ : @In BC a rl), @eq (list bool) (sem a xl (@nil (list bool))) (Sem (dummies (@length (list bool) xl) (@length (list bool) yl) (BC_to_Cobham (@length (list bool) xl) O a)) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  intros.
(* Goal: @eq (list bool) (sem a xl (@nil (list bool))) (Sem (dummies (@length (list bool) xl) (@length (list bool) yl) (BC_to_Cobham (@length (list bool) xl) O a)) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  rewrite dummies_correct.
(* Goal: @eq (list bool) (sem a xl (@nil (list bool))) (Sem (BC_to_Cobham (@length (list bool) xl) O a) (@firstn (list bool) (@length (list bool) xl) (@app (list bool) xl yl))) *)
(* Goal: le (@length (list bool) xl) (@length (list bool) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  erewrite H3; eauto.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  f_equal; subst; trivial.
(* Goal: @eq (list (list bool)) (@app (list bool) xl (@nil (list bool))) (@firstn (list bool) (@length (list bool) xl) (@app (list bool) xl yl)) *)
(* Goal: le (@length (list bool) xl) (@length (list bool) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  rewrite firstn_app.
(* Goal: @eq (list (list bool)) (@app (list bool) xl (@nil (list bool))) xl *)
(* Goal: le (@length (list bool) xl) (@length (list bool) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  apply app_nil_r.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite app_length; omega.
  assert (map (fun se : BC => sem se xl yl) tl =
    map (fun x : BC => Sem (BC_to_Cobham (length xl) (length yl) x) (xl ++ yl)) tl).
  apply map_ext2; intros; subst.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  eapply H4; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite H2, HA, H7; subst; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite map_length; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite map_length; trivial.
Qed.

Lemma app_prop : forall {A} (l2 l1 : list A) (P : A -> Prop),
  (fix f (l : list A) : Prop :=
  match l with
    | nil => True
    | e :: l' => P e /\ f l'
  end) l1  ->
  (fix f (l : list A) : Prop :=
  match l with
    | nil => True
    | e :: l' => P e /\ f l' 
  end) l2  ->  
  (fix f (l : list A) : Prop :=
  match l with
    | nil => True
    | e :: l' => P e /\ f l'
  end) (l1 ++ l2).
Proof.
(* Goal: forall (A : Type) (l2 l1 : list A) (P : forall _ : A, Prop) (_ : (fix f (l : list A) : Prop := match l with | nil => True | cons e l' => and (P e) (f l') end) l1) (_ : (fix f (l : list A) : Prop := match l with | nil => True | cons e l' => and (P e) (f l') end) l2), (fix f (l : list A) : Prop := match l with | nil => True | cons e l' => and (P e) (f l') end) (@app A l1 l2) *)
 induction l2; intros; simpl; auto.
(* Goal: (fix f (l : list A) : Prop := match l with | nil => True | cons e l' => and (P e) (f l') end) (@app A l1 (@nil A)) *)
(* Goal: (fix f (l : list A) : Prop := match l with | nil => True | cons e l' => and (P e) (f l') end) (@app A l1 (@cons A a l2)) *)
 simpl_list; auto.
(* Goal: (fix f (l : list A) : Prop := match l with | nil => True | cons e l' => and (P e) (f l') end) (@app A l1 (@cons A a l2)) *)
 replace (l1 ++ a :: l2) with ((l1 ++ [a]) ++ l2).
(* Goal: (fix f (l : list A) : Prop := match l with | nil => True | cons e l' => and (P e) (f l') end) (@app A (@app A l1 (@cons A a (@nil A))) l2) *)
(* Goal: @eq (list A) (@app A (@app A l1 (@cons A a (@nil A))) l2) (@app A l1 (@cons A a l2)) *)
 apply IHl2 with (P := P) (l1 := (l1 ++ [a])).
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
 induction l1; simpl.
(* Goal: (fix f (l : list A) : Prop := match l with | nil => True | cons e l' => and (P e) (f l') end) l2 *)
(* Goal: @eq (list A) (@app A (@app A l1 (@cons A a (@nil A))) l2) (@app A l1 (@cons A a l2)) *)
 tauto.
(* Goal: (fix f (l : list A) : Prop := match l with | nil => True | cons e l' => and (P e) (f l') end) l2 *)
(* Goal: @eq (list A) (@app A (@app A l1 (@cons A a (@nil A))) l2) (@app A l1 (@cons A a l2)) *)
 tauto.
(* Goal: (fix f (l : list A) : Prop := match l with | nil => True | cons e l' => and (P e) (f l') end) l2 *)
(* Goal: @eq (list A) (@app A (@app A l1 (@cons A a (@nil A))) l2) (@app A l1 (@cons A a l2)) *)
 tauto.
(* Goal: @eq (list A) (@app A (@app A l1 (@cons A a (@nil A))) l2) (@app A l1 (@cons A a l2)) *)
 apply app_ass.
Qed.

Lemma plusl_monotonic : forall l (f1 f2 : nat -> nat),
  (forall x, f1 x <= f2 x) ->
  plusl (map f1 l) <= plusl (map f2 l).
Proof.
(* Goal: forall _ : @eq nat (@length (list bool) l) n, @eq (list bool) (Sem (move_arg n i j e) l) (Sem e (@move_forward (list bool) i j l (Sem (Proj n O) l))) *)
 induction l; simpl; intros.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
 trivial.
(* Goal: le (Init.Nat.add (f1 a) (plusl (@map nat nat f1 l))) (Init.Nat.add (f2 a) (plusl (@map nat nat f2 l))) *)
 apply plus_le_compat.
(* Goal: le (f1 a) (f2 a) *)
(* Goal: le (plusl (@map nat nat f1 l)) (plusl (@map nat nat f2 l)) *)
 apply H.
(* Goal: le (plusl (@map nat nat f1 l)) (plusl (@map nat nat f2 l)) *)
 apply IHl.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
 trivial.
Qed.

Lemma BC_to_Cobham_bounded : forall (e : BC) n s,
  arities e = ok_arities n s ->
  rec_bounded' (BC_to_Cobham n s e).
Proof.
(* Goal: forall (a : BC) (_ : @In BC a rl), @eq (list bool) (sem a xl (@nil (list bool))) (Sem (dummies (@length (list bool) xl) (@length (list bool) yl) (BC_to_Cobham (@length (list bool) xl) O a)) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  apply BC_ind_inf; simpl BC_to_Cobham; intros.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  simpl; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  simpl; trivial.  
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  simpl; trivial.
  apply rec_bounded_Pred.
  apply rec_bounded_Cond.
  
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) xl) (@tl (list bool) xl) yl) (sem_Rec (Sem (BC_to_Cobham (Init.Nat.sub n O) s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) (Init.Nat.sub n O) (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) (@app (list bool) xl yl)) (@tl (list bool) (@app (list bool) xl yl))) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  simpl; rewrite <- minus_n_O.

  split.
  apply rec_bounded_spec.
  apply rec_bounded_Poly.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  split; trivial.
  split.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  apply rec_bounded_move_arg; trivial.
  split.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  apply rec_bounded_move_arg; trivial.

  erewrite arity_BC_to_Cobham; eauto.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite move_arg_inf; try omega.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite move_arg_inf; try omega.
  rewrite arity_Poly.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  simpl.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  repeat rewrite <- beq_nat_refl; simpl.
  erewrite arity_poly_BC; eauto.
  erewrite arity_poly_BC; eauto.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  simpl.
  erewrite arity_poly_BC; eauto.
  repeat rewrite Nat.max_idempotent.
  rewrite parity_psum.
  rewrite max_l; [ | omega].
  rewrite plus_Sn_m.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite <- beq_nat_refl; trivial.

(* Goal: forall (a : BC) (_ : @In BC a rl), @eq (list bool) (sem a xl (@nil (list bool))) (Sem (dummies (@length (list bool) xl) (@length (list bool) yl) (BC_to_Cobham (@length (list bool) xl) O a)) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  intros.
  rewrite Poly_correct.

  rewrite pplus_correct, pplus_correct, pmult_correct, pplus_correct.
  rewrite pproj_correct, pshift_correct.

  assert (length (hd nil l) = nth 0 (map (@length _) l) 0).
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (@nth (list bool) O l (@nil bool))) *)
  rewrite <- hd_nth_0.
  change 0 with (@length bool nil).
  apply map_hd.
  rewrite <- H6.
  clear H6.

  rewrite <- plus_Sn_m in H5.
  apply length_plus_ex in H5.
  destruct H5 as [l1 [l2 [Hl1 [Hl2 Hl]]]].
  rewrite Hl.

  change (S n) with (1 + n) in Hl1.
  apply length_plus_ex in Hl1.
  destruct Hl1 as [l1a [l1b [Hl1a [Hl1b Hl1]]]].
  destruct l1a.
(* Goal: @eq (list bool) (sem g (@nil (list bool)) yl) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) yl) (@tl (list bool) yl)) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) l (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  simpl in Hl1a; discriminate.  

  rewrite Hl1.
  simpl hd.
  simpl tl.

  assert (l1a = nil).
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  destruct l1a; trivial.
(* Goal: @eq (list bool) (sem g (@nil (list bool)) yl) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) yl) (@tl (list bool) yl)) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) l (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  simpl in Hl1a; discriminate.
  clear Hl1a.

  assert (tl (l1 ++ l2) = tl l1 ++ l2).
  apply tl_app.
(* Goal: @eq (list bool) (sem g (@nil (list bool)) yl) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) (@hd (list bool) (@nil bool) yl) (@tl (list bool) yl)) *)
(* Goal: @eq (list bool) (sem_rec (sem g) (sem h0) (sem h1) l xl yl) (sem_Rec (Sem (BC_to_Cobham n s g)) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h0))) (Sem (move_arg (S (S (Init.Nat.add n s))) (S O) n (BC_to_Cobham (S n) (S s) h1))) l (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  intro; subst; simpl in *; discriminate.
  
  assert (tl l1 = l1b).
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite Hl1, H5; simpl; trivial.
  clear Hl1.

(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  induction l0; simpl.

  rewrite H5 in *; simpl in *.

  erewrite <- BC_to_Cobham_correct; eauto.
  eapply le_trans.
  eapply polymax_bounding; eauto.
  rewrite plus_comm.
(* Goal: le (Init.Nat.add (f1 a) (plusl (@map nat nat f1 l))) (Init.Nat.add (f2 a) (plusl (@map nat nat f2 l))) *)
  apply plus_le_compat.
  rewrite psum_correct.
  eapply le_trans.
  apply maxl_le_plusl.
  rewrite map_nth_seq.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  simpl.
  rewrite <- map_skipn.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite <- Hl1b; simpl.
  rewrite skipn_app.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  trivial.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  simpl.
  rewrite map_length.
  rewrite app_length.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  rewrite Hl1b, Hl2; omega.
(* Goal: @eq Arity (ok_arity n) (ok_arity (Init.Nat.add n O)) *)
(* Goal: @eq Arity (if andb (Nat.eqb n' (@length Cobham (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n')))) (andb (Nat.eqb (Init.Nat.add n' n) (Init.Nat.add n' n)) (@forallb Arity (fun e : Arity => arity_eq e (ok_arity (S (Init.Nat.add n' n)))) (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n'))))) then ok_arity (S (Init.Nat.add n' n)) else error_Comp (ok_arity (S n')) (@cons Arity (ok_arity (S (Init.Nat.add n' n))) (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n'))))) (ok_arity (Init.Nat.add n (S n'))) *)
  rewrite plus_0_r.
  rewrite <- (app_nil_r (map (@length _) l1b)) at 1.
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  rewrite map_app.
  erewrite parity_correct.
  apply le_refl.
  eapply pWF_poly_BC; eauto.
  erewrite arity_poly_BC; eauto.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite map_length; trivial.

  remember ( sem_Rec (Sem (BC_to_Cobham n s g))
    (Sem (move_arg (S (S (n + s))) 1 n (BC_to_Cobham (S n) (S s) h0)))
    (Sem (move_arg (S (S (n + s))) 1 n (BC_to_Cobham (S n) (S s) h1))) l0 
    ((l1a ++ l1b) ++ l2)) as r.

(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  repeat rewrite move_arg_correct; simpl.

  assert (move_forward 1 n (l0 :: r :: (l1a ++ l1b) ++ l2) l0 = ((l0 :: (l1a ++ l1b)) ++ (r :: l2))).
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  unfold move_forward; simpl.
(* Goal: @eq (list bool) (Sem e (@map nat (list bool) (fun x : nat => @nth (list bool) x l (@nil bool)) (seq O n))) (Sem e (@firstn (list bool) n l)) *)
  f_equal.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite H5; simpl.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite <- Hl1b, firstn_app, skipn_app; trivial.
  rewrite H8; clear H8.

  assert ( maxl (map (@length _) (r :: l2)) <= 
    peval (psum (S n) s) (S (length l0) :: map (@length _) ((l1a ++ l1b) ++ l2)) +
    (peval (poly_BC n g) (map (@length _) ((l1a ++ l1b) ++ l2)) +
      length l0 *
      (peval (poly_BC (S n) h0) (S (length l0) :: map (@length _) ((l1a ++ l1b) ++ l2)) +
        peval (poly_BC (S n) h1) (S (length l0) :: map (@length _) ((l1a ++ l1b) ++ l2))))).
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  simpl.

  apply Nat.max_lub.

  eapply le_trans.
  eapply IHl0.
  rewrite psum_correct.
  rewrite psum_correct.
(* Goal: le (Init.Nat.add (f1 a) (plusl (@map nat nat f1 l))) (Init.Nat.add (f2 a) (plusl (@map nat nat f2 l))) *)
  apply plus_le_compat.
  apply plusl_monotonic.
(* Goal: @eq (list bool) (sem cond (@nil (list bool)) l) (Sem Cond l) *)
  intros; simpl.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  destruct x; trivial.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  omega.
  apply plus_le_compat_l.
  apply mult_le_compat_l.
(* Goal: le (Init.Nat.add (f1 a) (plusl (@map nat nat f1 l))) (Init.Nat.add (f2 a) (plusl (@map nat nat f2 l))) *)
  apply plus_le_compat.
(* Goal: @eq (list bool) (sem cond (@nil (list bool)) l) (Sem Cond l) *)
  apply peval_monotonic; intros; simpl.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  destruct i; omega.
(* Goal: @eq (list bool) (sem cond (@nil (list bool)) l) (Sem Cond l) *)
  apply peval_monotonic; intros; simpl.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  destruct i; omega.

  apply le_plus_trans.
  rewrite psum_correct.
  eapply le_trans.
  apply maxl_le_plusl.
  rewrite map_nth_seq.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  simpl.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite H5, <- Hl1b; simpl.
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) xl yl)) (@app Cobham (@map BC Cobham (fun e : BC => dummies n s (BC_to_Cobham n O e)) rl) (@map BC Cobham (BC_to_Cobham n s) tl)))) *)
  rewrite map_app.
  erewrite <- map_length.
  rewrite skipn_app.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  trivial.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  simpl.
  rewrite map_length.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite H5, <- Hl1b, <- Hl2; simpl.
(* Goal: @eq nat (S (Init.Nat.add n' n)) (Init.Nat.add n (S n')) *)
(* Goal: @eq Arity (error_Comp (ok_arity (S n')) (@cons Arity (ok_arity (S (Init.Nat.add n' n))) (@map Cobham Arity arity (@map nat Cobham (Proj (S (Init.Nat.add n' n))) (seq (S O) n'))))) (ok_arity (Init.Nat.add n (S n'))) *)
  rewrite app_length; ring. 

  case a.

  erewrite <- BC_to_Cobham_correct; simpl; eauto.
  eapply le_trans.
  eapply polymax_bounding; eauto.
  assert ( peval (poly_BC (S n) h1) (map (@length _) (l0 :: l1a ++ l1b)) <=  
    peval (poly_BC (S n) h1)  (S (length l0) :: map (@length _) ((l1a ++ l1b) ++ l2))).
  apply peval_monotonic.
(* Goal: forall (a : BC) (_ : @In BC a rl), @eq (list bool) (sem a xl (@nil (list bool))) (Sem (dummies (@length (list bool) xl) (@length (list bool) yl) (BC_to_Cobham (@length (list bool) xl) O a)) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  intros.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  simpl.
  destruct i.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  omega.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite H5; simpl.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  repeat rewrite map_nth2 with (d := nil); simpl; trivial.
  apply length_nth_app.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  omega.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite <- Hl1b, H5; simpl; trivial.

  erewrite <- BC_to_Cobham_correct; simpl; eauto.
  eapply le_trans.
  eapply polymax_bounding; eauto.
  assert ( peval (poly_BC (S n) h0) (map (@length _) (l0 :: l1a ++ l1b)) <=  
    peval (poly_BC (S n) h0)  (S (length l0) :: map (@length _) ((l1a ++ l1b) ++ l2))).
  apply peval_monotonic.
(* Goal: forall (a : BC) (_ : @In BC a rl), @eq (list bool) (sem a xl (@nil (list bool))) (Sem (dummies (@length (list bool) xl) (@length (list bool) yl) (BC_to_Cobham (@length (list bool) xl) O a)) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  intros.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  simpl.
  destruct i.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  omega.
(* Goal: @eq bool (arity_eq (arity (Proj (S (Init.Nat.add n' n)) p)) (ok_arity (S (Init.Nat.add n' n)))) true *)
  rewrite H5; simpl.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  repeat rewrite map_nth2 with (d := nil); simpl; trivial.
  apply length_nth_app.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  omega.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite <- Hl1b, H5; simpl; trivial.

(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite <- Hl1b, <- Hl2, H5, app_length; simpl; trivial.
(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  rewrite <- Hl1b, <- Hl2, H5, app_length; simpl; trivial.

  pWF; eapply pWF_poly_BC; eauto.

(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  erewrite arity_BC_to_Cobham; eauto; f_equal; omega.
(* Goal: lt i n *)
(* Goal: lt (Init.Nat.add i j) (@length Cobham (@map nat Cobham (Proj n) (seq O n))) *)
  erewrite arity_BC_to_Cobham; eauto; f_equal; omega.

  simpl in *.

(* Goal: forall x : nat, le (f1 x) (f2 x) *)
  split; trivial.
  clear H H2.
  apply app_prop with 
  (l1 := (map (fun e0 : BC => dummies n s (BC_to_Cobham n 0 e0)) rl))
  (l2 := map (BC_to_Cobham n s) tl)
  (P := rec_bounded').
  induction rl; simpl; auto.
  split.
  apply rec_bounded_dummies.
  apply H3; simpl; auto.
(* Goal: forall (a : BC) (_ : @In BC a rl), @eq (list bool) (sem a xl (@nil (list bool))) (Sem (dummies (@length (list bool) xl) (@length (list bool) yl) (BC_to_Cobham (@length (list bool) xl) O a)) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  apply IHrl; intros.
  apply H0; simpl; auto.
  apply H3; simpl; auto.
  induction tl; simpl; auto.
  split.
  apply H4; simpl; auto.
(* Goal: forall (a : BC) (_ : @In BC a rl), @eq (list bool) (sem a xl (@nil (list bool))) (Sem (dummies (@length (list bool) xl) (@length (list bool) yl) (BC_to_Cobham (@length (list bool) xl) O a)) (@app (list bool) xl yl)) *)
(* Goal: @eq (list bool) (sem h (@map BC (list bool) (fun ne : BC => sem ne xl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se xl yl) tl)) (Sem (BC_to_Cobham (@length BC rl) (@length BC tl) h) (@app (list bool) (@map BC (list bool) (fun x : BC => Sem (dummies n s (BC_to_Cobham n O x)) (@app (list bool) xl yl)) rl) (@map BC (list bool) (fun x : BC => Sem (BC_to_Cobham n s x) (@app (list bool) xl yl)) tl))) *)
  apply IHtl; intros.
  apply H1; simpl; auto.
  apply H4; simpl; auto.
Qed.
