Require Import Coq.Sorting.Permutation.
Require Import Coq.Sorting.Sorting.
Require Import Coq.Structures.Orders.
Require Import VST.veric.Clight_base.
Require Import VST.veric.Clight_lemmas.
Require Import VST.veric.type_induction.
Require Import VST.veric.composite_compute.
Require Import VST.veric.align_mem.
Require Import VST.veric.tycontext.
Require Import VST.veric.Cop2.

Section cs_preserve.

Context (cs_from cs_to: compspecs).

Definition test_aux (b: bool) (i: ident): bool :=
  b && match (@cenv_cs cs_from) ! i, (@cenv_cs cs_to) ! i with
       | Some co_from, Some co_to => eqb_list eqb_member (co_members co_from) (co_members co_to) && eqb_su (co_su co_from) (co_su co_to) && eqb_attr (co_attr co_from) (co_attr co_to)
       | _, _ => false
       end.

Fixpoint cs_preserve_type (coeq: PTree.t bool) (t: type): bool :=
  match t with
  | Tarray t0 _ _ => cs_preserve_type coeq t0
  | Tstruct id _ => match coeq ! id with | Some b => test_aux b id | _ => false end
  | Tunion id _ => match coeq ! id with | Some b => test_aux b id | _ => false end
  | _ => true
  end.

Fixpoint cs_preserve_members (coeq: PTree.t bool) (m: members): bool :=
  match m with
  | nil => true
  | ((_, t) :: m) => andb (cs_preserve_type coeq t) (cs_preserve_members coeq m)
  end.

Class change_composite_env: Type := {
  coeq: PTree.t bool;
  coeq_consistent:
    forall i co b,
      (@cenv_cs cs_to) ! i = Some co ->
      coeq ! i = Some b ->
      b = cs_preserve_members coeq (co_members co);
  coeq_complete:
    forall i,
      (exists co, (@cenv_cs cs_to) ! i = Some co) <->
      (exists b, coeq ! i = Some b)
}.

Definition cs_preserve_env: PTree.t bool :=
  let l := composite_reorder.rebuild_composite_elements (@cenv_cs cs_to) in
  fold_right (fun (ic: positive * composite) (T0: PTree.t bool) => let (i, co) := ic in let T := T0 in PTree.set i (cs_preserve_members T (co_members co)) T) (PTree.empty _) l.

Lemma aux1: forall T co,
  (fix fm (l : list (ident * type * bool)) : bool :=
   match l with
   | nil => true
   | (_, _, b) :: l' => b && fm l'
   end)
  (map
     (fun it0 : positive * type =>
      let (i0, t0) := it0 in
      (i0, t0,
      type_func.F (fun t : type => match t with | Tstruct _ _ | Tunion _ _ => false | _ => true end) (fun (b : bool) (_ : type) (_ : Z) (_ : attr) => b)
        (fun (b : bool) (id : ident) (_ : attr) => test_aux b id)
        (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) T t0)) (co_members co)) =
  cs_preserve_members T (co_members co).
Proof.
(* Goal: forall (T : PTree.t bool) (co : composite), @eq bool ((fix fm (l : list (prod (prod ident type) bool)) : bool := match l with | nil => true | cons (pair (pair i t as p0) b as p) l' => andb b (fm l') end) (@map (prod positive type) (prod (prod positive type) bool) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) bool (@pair positive type i0 t0) (@type_func.F bool (fun t : type => match t with | Tvoid => true | Tint i s a => true | Tlong s a => true | Tfloat f a => true | Tpointer t1 a => true | Tarray t1 z a => true | Tfunction t1 t2 c => true | Tstruct i a => false | Tunion i a => false end) (fun (b : bool) (_ : type) (_ : Z) (_ : attr) => b) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) T t0)) (co_members co))) (cs_preserve_members T (co_members co)) *)
  intros; unfold cs_preserve_members, cs_preserve_type, type_func.F.
(* Goal: @eq bool ((fix fm (l : list (prod (prod ident type) bool)) : bool := match l with | nil => true | cons (pair (pair i t as p0) b as p) l' => andb b (fm l') end) (@map (prod positive type) (prod (prod positive type) bool) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) bool (@pair positive type i0 t0) ((fix F (env : PTree.t bool) (t : type) {struct t} : bool := match t with | Tvoid => match t with | Tvoid => true | Tint i s a => true | Tlong s a => true | Tfloat f a => true | Tpointer t1 a => true | Tarray t1 z a => true | Tfunction t1 t2 c => true | Tstruct i a => false | Tunion i a => false end | Tint i s a => match t with | Tvoid => true | Tint i1 s0 a0 => true | Tlong s0 a0 => true | Tfloat f a0 => true | Tpointer t1 a0 => true | Tarray t1 z a0 => true | Tfunction t1 t2 c => true | Tstruct i1 a0 => false | Tunion i1 a0 => false end | Tlong s a => match t with | Tvoid => true | Tint i s0 a0 => true | Tlong s0 a0 => true | Tfloat f a0 => true | Tpointer t1 a0 => true | Tarray t1 z a0 => true | Tfunction t1 t2 c => true | Tstruct i a0 => false | Tunion i a0 => false end | Tfloat f a => match t with | Tvoid => true | Tint i s a0 => true | Tlong s a0 => true | Tfloat f0 a0 => true | Tpointer t1 a0 => true | Tarray t1 z a0 => true | Tfunction t1 t2 c => true | Tstruct i a0 => false | Tunion i a0 => false end | Tpointer t1 a => match t with | Tvoid => true | Tint i s a0 => true | Tlong s a0 => true | Tfloat f a0 => true | Tpointer t2 a0 => true | Tarray t2 z a0 => true | Tfunction t2 t3 c => true | Tstruct i a0 => false | Tunion i a0 => false end | Tarray t1 n a => F env t1 | Tfunction t1 t2 c => match t with | Tvoid => true | Tint i s a => true | Tlong s a => true | Tfloat f a => true | Tpointer t3 a => true | Tarray t3 z a => true | Tfunction t3 t4 c0 => true | Tstruct i a => false | Tunion i a => false end | Tstruct id a => match @PTree.get bool id env with | Some v => test_aux v id | None => match t with | Tvoid => true | Tint i s a0 => true | Tlong s a0 => true | Tfloat f a0 => true | Tpointer t1 a0 => true | Tarray t1 z a0 => true | Tfunction t1 t2 c => true | Tstruct i a0 => false | Tunion i a0 => false end end | Tunion id a => match @PTree.get bool id env with | Some v => test_aux v id | None => match t with | Tvoid => true | Tint i s a0 => true | Tlong s a0 => true | Tfloat f a0 => true | Tpointer t1 a0 => true | Tarray t1 z a0 => true | Tfunction t1 t2 c => true | Tstruct i a0 => false | Tunion i a0 => false end end end) T t0)) (co_members co))) ((fix cs_preserve_members (coeq : PTree.t bool) (m : members) {struct m} : bool := match m with | nil => true | cons (pair i t as p) m0 => andb ((fix cs_preserve_type (coeq0 : PTree.t bool) (t0 : type) {struct t0} : bool := match t0 with | Tvoid => true | Tint i0 s a => true | Tlong s a => true | Tfloat f a => true | Tpointer t1 a => true | Tarray t1 z a => cs_preserve_type coeq0 t1 | Tfunction t1 t2 c => true | Tstruct id a => match @PTree.get bool id coeq0 with | Some b => test_aux b id | None => false end | Tunion id a => match @PTree.get bool id coeq0 with | Some b => test_aux b id | None => false end end) coeq t) (cs_preserve_members coeq m0) end) T (co_members co)) *)
  induction (co_members co) as [| [i t] ?].
  + auto.
  + simpl.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    f_equal; auto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    induction t; auto.
Qed.

Lemma aux2:
  type_func.Env (fun t : type => match t with | Tstruct _ _ | Tunion _ _ => false | _ => true end) (fun (b : bool) (_ : type) (_ : Z) (_ : attr) => b)
        (fun (b : bool) (id : ident) (_ : attr) => test_aux b id)
        (fun (b : bool) (id : ident) (_ : attr) => test_aux b id)
        (fun _ : struct_or_union =>
         fix fm (l : list (ident * type * bool)) : bool :=
           match l with
           | nil => true
           | (_, _, b) :: l' => b && fm l'
           end) (composite_reorder.rebuild_composite_elements cenv_cs) =
  cs_preserve_env.
Proof.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  intros.
(* Goal: @eq (PTree.t bool) (@type_func.Env bool (fun t : type => match t with | Tvoid => true | Tint i s a => true | Tlong s a => true | Tfloat f a => true | Tpointer t0 a => true | Tarray t0 z a => true | Tfunction t0 t1 c => true | Tstruct i a => false | Tunion i a => false end) (fun (b : bool) (_ : type) (_ : Z) (_ : attr) => b) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) (fun _ : struct_or_union => fix fm (l : list (prod (prod ident type) bool)) : bool := match l with | nil => true | cons (pair (pair i t as p0) b as p) l' => andb b (fm l') end) (composite_reorder.rebuild_composite_elements (@cenv_cs cs_to))) cs_preserve_env *)
  unfold type_func.Env, type_func.env_rec, cs_preserve_env.
(* Goal: @eq Z (align z (@alignof (@cenv_cs cs_from) t0)) (align z (@alignof (@cenv_cs cs_to) t0)) *)
  f_equal.
(* Goal: @eq (forall (_ : prod positive composite) (_ : PTree.t bool), PTree.t bool) (fun ic : prod positive composite => let (i, co) := ic in fun env : PTree.t bool => @PTree.set bool i ((fix fm (l : list (prod (prod ident type) bool)) : bool := match l with | nil => true | cons (pair (pair i0 t as p0) b as p) l' => andb b (fm l') end) (@map (prod positive type) (prod (prod positive type) bool) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) bool (@pair positive type i0 t0) (@type_func.F bool (fun t : type => match t with | Tvoid => true | Tint i1 s a => true | Tlong s a => true | Tfloat f a => true | Tpointer t1 a => true | Tarray t1 z a => true | Tfunction t1 t2 c => true | Tstruct i1 a => false | Tunion i1 a => false end) (fun (b : bool) (_ : type) (_ : Z) (_ : attr) => b) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) env t0)) (co_members co))) env) (fun (ic : prod positive composite) (T0 : PTree.t bool) => let (i, co) := ic in @PTree.set bool i (cs_preserve_members T0 (co_members co)) T0) *)
  extensionality ic.
(* Goal: @eq (forall _ : PTree.t bool, PTree.t bool) (let (i, co) := ic in fun env : PTree.t bool => @PTree.set bool i ((fix fm (l : list (prod (prod ident type) bool)) : bool := match l with | nil => true | cons (pair (pair i0 t as p0) b as p) l' => andb b (fm l') end) (@map (prod positive type) (prod (prod positive type) bool) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) bool (@pair positive type i0 t0) (@type_func.F bool (fun t : type => match t with | Tvoid => true | Tint i1 s a => true | Tlong s a => true | Tfloat f a => true | Tpointer t1 a => true | Tarray t1 z a => true | Tfunction t1 t2 c => true | Tstruct i1 a => false | Tunion i1 a => false end) (fun (b : bool) (_ : type) (_ : Z) (_ : attr) => b) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) env t0)) (co_members co))) env) (fun T0 : PTree.t bool => let (i, co) := ic in @PTree.set bool i (cs_preserve_members T0 (co_members co)) T0) *)
  destruct ic as [i co].
(* Goal: @eq (forall _ : PTree.t bool, PTree.t bool) (fun env : PTree.t bool => @PTree.set bool i ((fix fm (l : list (prod (prod ident type) bool)) : bool := match l with | nil => true | cons (pair (pair i t as p0) b as p) l' => andb b (fm l') end) (@map (prod positive type) (prod (prod positive type) bool) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) bool (@pair positive type i0 t0) (@type_func.F bool (fun t : type => match t with | Tvoid => true | Tint i s a => true | Tlong s a => true | Tfloat f a => true | Tpointer t1 a => true | Tarray t1 z a => true | Tfunction t1 t2 c => true | Tstruct i a => false | Tunion i a => false end) (fun (b : bool) (_ : type) (_ : Z) (_ : attr) => b) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) env t0)) (co_members co))) env) (fun T0 : PTree.t bool => @PTree.set bool i (cs_preserve_members T0 (co_members co)) T0) *)
  extensionality T.
(* Goal: @eq Z (align z (@alignof (@cenv_cs cs_from) t0)) (align z (@alignof (@cenv_cs cs_to) t0)) *)
  f_equal.
(* Goal: @eq bool ((fix fm (l : list (prod (prod ident type) bool)) : bool := match l with | nil => true | cons (pair (pair i t as p0) b as p) l' => andb b (fm l') end) (@map (prod positive type) (prod (prod positive type) bool) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) bool (@pair positive type i0 t0) (@type_func.F bool (fun t : type => match t with | Tvoid => true | Tint i s a => true | Tlong s a => true | Tfloat f a => true | Tpointer t1 a => true | Tarray t1 z a => true | Tfunction t1 t2 c => true | Tstruct i a => false | Tunion i a => false end) (fun (b : bool) (_ : type) (_ : Z) (_ : attr) => b) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) (fun (b : bool) (id : ident) (_ : attr) => test_aux b id) T t0)) (co_members co))) (cs_preserve_members T (co_members co)) *)
  apply aux1.
Qed.

Lemma cs_preserve_env_consisent: forall (coeq: PTree.t bool),
  coeq = cs_preserve_env ->
  forall i co b,
    (@cenv_cs cs_to) ! i = Some co ->
    coeq ! i = Some b ->
    b = cs_preserve_members coeq (co_members co).
Proof.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  intros.
  pose proof @composite_reorder_consistent bool (@cenv_cs cs_to)
             (fun t : type => match t with | Tstruct _ _ | Tunion _ _ => false | _ => true end)
             (fun b _ _ _ => b)
             (fun b id _ => test_aux b id)
             (fun b id _ => test_aux b id)
             (fun _ =>
                fix fm (l: list (ident * type * bool)): bool :=
                match l with
                | nil => true
                | (_, _, b) :: l' => b && (fm l')
                end)
             (@cenv_consistent cs_to)
    as HH.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i coeq0) (@Some bool b))) *)
  hnf in HH.
(* Goal: @eq bool b (cs_preserve_members coeq0 (co_members co)) *)
  subst coeq0.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
  rewrite aux2 in HH.
(* Goal: @eq bool b (cs_preserve_members cs_preserve_env (co_members co)) *)
  specialize (HH _ _ b H0 H1).
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
  rewrite HH, aux1; auto.
Qed.

Lemma cs_preserve_completeness: forall (coeq: PTree.t bool),
  coeq = cs_preserve_env ->
  forall i,
    (exists co, (@cenv_cs cs_to) ! i = Some co) <->
    (exists b, coeq ! i = Some b).
Proof.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  intros.
  pose proof @composite_reorder_complete bool (@cenv_cs cs_to)
             (fun t : type => match t with | Tstruct _ _ | Tunion _ _ => false | _ => true end)
             (fun b _ _ _ => b)
             (fun b id _ => test_aux b id)
             (fun b id _ => test_aux b id)
             (fun _ =>
                fix fm (l: list (ident * type * bool)): bool :=
                match l with
                | nil => true
                | (_, _, b) :: l' => b && (fm l')
                end)
    as HH.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i coeq0) (@Some bool b))) *)
  hnf in HH.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) t ofs) (align_compatible_rec (@cenv_cs cs_to) t ofs) *)
  subst.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
  rewrite aux2 in HH.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
  auto.
Qed.

End cs_preserve.

Ltac make_cs_preserve cs_from cs_to :=
  let coeq0 := eval cbv in (cs_preserve_env cs_from cs_to) in
  let Hcoeq0 := constr: (eq_refl: coeq0 = cs_preserve_env cs_from cs_to) in
  let coeq0_consistent := constr: (cs_preserve_env_consisent cs_from cs_to coeq0 Hcoeq0) in
  let coeq0_complete := constr: (cs_preserve_completeness cs_from cs_to coeq0 Hcoeq0) in
  refine (  {| coeq := coeq0 ;
               coeq_consistent := coeq0_consistent;
               coeq_complete := coeq0_complete |}).

Lemma sizeof_composite_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall su (m: members),
  Forall
       (Basics.compose
          (fun t : type =>
           cs_preserve_type cs_from cs_to (coeq cs_from cs_to) t = true ->
           @sizeof (@cenv_cs cs_from) t = @sizeof (@cenv_cs cs_to) t /\
           @alignof (@cenv_cs cs_from) t = @alignof (@cenv_cs cs_to) t) snd) m ->
  true = cs_preserve_members cs_from cs_to (coeq cs_from cs_to) m ->
  sizeof_composite (@cenv_cs cs_from) su m = sizeof_composite (@cenv_cs cs_to) su m.
Proof.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  intros.
(* Goal: @eq Z (alignof_composite (@cenv_cs cs_from) m) (alignof_composite (@cenv_cs cs_to) m) *)
  symmetry in H0.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
  destruct su; simpl; auto.
  + generalize 0 as z.
(* Goal: @eq Z (alignof_composite (@cenv_cs cs_from) m) (alignof_composite (@cenv_cs cs_to) m) *)
    induction H as [| [i t] ? ?]; intros; [reflexivity |].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tarray t z a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tarray t z a) ofs) *)
    simpl.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
    simpl in H0.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
    rewrite andb_true_iff in H0.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
    destruct H0.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
    apply H in H0; clear H; simpl in H0; destruct H0.
(* Goal: @eq Z (sizeof_struct (@cenv_cs cs_from) (Z.add (align z (@alignof (@cenv_cs cs_from) t)) (@sizeof (@cenv_cs cs_from) t)) l) (sizeof_struct (@cenv_cs cs_to) (Z.add (align z (@alignof (@cenv_cs cs_to) t)) (@sizeof (@cenv_cs cs_to) t)) l) *)
    rewrite H, H0.
    apply (IHForall H2 (align z (alignof t) + sizeof t)).
  + induction H as [| [i t] ? ?]; intros; [reflexivity |].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tarray t z a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tarray t z a) ofs) *)
    simpl.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
    simpl in H0.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
    rewrite andb_true_iff in H0.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
    destruct H0.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
    apply H in H0; clear H; simpl in H0; destruct H0.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    f_equal; auto.
Qed.

Lemma alignof_composite_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall (m: members),
  Forall
       (Basics.compose
          (fun t : type =>
           cs_preserve_type cs_from cs_to (coeq cs_from cs_to) t = true ->
           @sizeof (@cenv_cs cs_from) t = @sizeof (@cenv_cs cs_to) t /\
           @alignof (@cenv_cs cs_from) t = @alignof (@cenv_cs cs_to) t) snd) m ->
  true = cs_preserve_members cs_from cs_to (coeq cs_from cs_to) m ->
  alignof_composite (@cenv_cs cs_from) m = alignof_composite (@cenv_cs cs_to) m.
Proof.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  intros.
(* Goal: @eq Z (alignof_composite (@cenv_cs cs_from) m) (alignof_composite (@cenv_cs cs_to) m) *)
  symmetry in H0.
(* Goal: @eq Z (alignof_composite (@cenv_cs cs_from) m) (alignof_composite (@cenv_cs cs_to) m) *)
  induction H as [| [i t] ? ?]; intros; [reflexivity |].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tarray t z a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tarray t z a) ofs) *)
  simpl.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
  simpl in H0.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
  rewrite andb_true_iff in H0.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
  destruct H0.
(* Goal: @eq Z (Z.max (@alignof (@cenv_cs cs_from) t) (alignof_composite (@cenv_cs cs_from) l)) (Z.max (@alignof (@cenv_cs cs_to) t) (alignof_composite (@cenv_cs cs_to) l)) *)
  apply H in H0; clear H; simpl in H0; destruct H0.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
  f_equal; auto.
Qed.

Lemma sizeof_alignof_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  @sizeof (@cenv_cs cs_from) t = @sizeof (@cenv_cs cs_to) t /\
  @alignof (@cenv_cs cs_from) t = @alignof (@cenv_cs cs_to) t.
Proof.
(* Goal: forall (t : type) (_ : @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) t) true) (ofs : Z), iff (align_compatible_rec (@cenv_cs cs_from) t ofs) (align_compatible_rec (@cenv_cs cs_to) t ofs) *)
  intros t.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  type_induction t (@cenv_cs cs_to) (@cenv_consistent cs_to); intros.
  + split; reflexivity.
  + split; reflexivity.
  + split; reflexivity.
  + split; reflexivity.
  + split; reflexivity.
  + simpl.
(* Goal: and (@eq Z (Z.mul (@sizeof (@cenv_cs cs_from) t) (Z.max Z0 z)) (Z.mul (@sizeof (@cenv_cs cs_to) t) (Z.max Z0 z))) (@eq Z (align_attr a (@alignof (@cenv_cs cs_from) t)) (align_attr a (@alignof (@cenv_cs cs_to) t))) *)
    pose proof IH H as [? ?].
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    split; f_equal; auto.
  + split; reflexivity.
  + simpl in *.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    unfold test_aux in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    destruct ((@cenv_cs cs_to) ! id) eqn:?H.
    - pose proof proj1 (coeq_complete _ _ _) (ex_intro _ _ H0) as [b ?H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      rewrite H1 in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct b; [| inv H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct ((@cenv_cs cs_from) ! id) eqn:?H; [| inv H].
(* Goal: and (@eq Z (co_sizeof c0) (co_sizeof c)) (@eq Z (align_attr a (co_alignof c0)) (align_attr a (co_alignof c))) *)
      rewrite (co_consistent_sizeof (@cenv_cs cs_to) c (@cenv_consistent cs_to _ _ H0)).
(* Goal: and (@eq Z (co_sizeof c0) (align (sizeof_composite (@cenv_cs cs_to) (co_su c) (co_members c)) (co_alignof c))) (@eq Z (align_attr a (co_alignof c0)) (align_attr a (co_alignof c))) *)
      rewrite (co_consistent_sizeof (@cenv_cs cs_from) c0 (@cenv_consistent cs_from _ _ H2)).
(* Goal: and (@eq Z (align (sizeof_composite (@cenv_cs cs_from) (co_su c0) (co_members c0)) (co_alignof c0)) (align (sizeof_composite (@cenv_cs cs_to) (co_su c) (co_members c)) (co_alignof c))) (@eq Z (align_attr a (co_alignof c0)) (align_attr a (co_alignof c))) *)
      rewrite (co_consistent_alignof (@cenv_cs cs_to) c (@cenv_consistent cs_to _ _ H0)).
(* Goal: and (@eq Z (align (sizeof_composite (@cenv_cs cs_from) (co_su c0) (co_members c0)) (co_alignof c0)) (align (sizeof_composite (@cenv_cs cs_to) (co_su c) (co_members c)) (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) (@eq Z (align_attr a (co_alignof c0)) (align_attr a (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) *)
      rewrite (co_consistent_alignof (@cenv_cs cs_from) c0 (@cenv_consistent cs_from _ _ H2)).
(* Goal: @eq bool true (cs_preserve_members cs_from cs_to (@coeq cs_from cs_to CCE) m) *)
      simpl in H.
(* Goal: and (@eq Z (align (sizeof_composite (@cenv_cs cs_from) (co_su c0) (co_members c0)) (align_attr (co_attr c0) (alignof_composite (@cenv_cs cs_from) (co_members c0)))) (align (sizeof_composite (@cenv_cs cs_to) (co_su c) (co_members c)) (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) (@eq Z (align_attr a (align_attr (co_attr c0) (alignof_composite (@cenv_cs cs_from) (co_members c0)))) (align_attr a (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) *)
      rewrite !andb_true_iff in H; destruct H as [[? ?] ?].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_list_spec in H; [| apply eqb_member_spec].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_su_spec in H3.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_attr_spec in H4.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply (coeq_consistent _ _ _ _ _ H0) in H1.
      rewrite H in *; rewrite H4 in  *; rewrite H3 in *; clear c0 H H0 H2 H3 H4.
(* Goal: and (@eq Z (align (sizeof_composite (@cenv_cs cs_from) (co_su c) (co_members c)) (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_from) (co_members c)))) (align (sizeof_composite (@cenv_cs cs_to) (co_su c) (co_members c)) (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) (@eq Z (align_attr a (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_from) (co_members c)))) (align_attr a (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) *)
      split; [f_equal; [ | f_equal] | f_equal; f_equal].
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      * apply sizeof_composite_change_composite; auto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      * apply alignof_composite_change_composite; auto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      * apply alignof_composite_change_composite; auto.
    - destruct ((coeq cs_from cs_to) ! id) eqn:?H.
      * pose proof proj2 (coeq_complete _ _ id) (ex_intro _ b H1) as [co ?].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
        congruence.
      * inv H.
  + simpl in *.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    unfold test_aux in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    destruct ((@cenv_cs cs_to) ! id) eqn:?H.
    - pose proof proj1 (coeq_complete _ _ _) (ex_intro _ _ H0) as [b ?H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      rewrite H1 in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct b; [| inv H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct ((@cenv_cs cs_from) ! id) eqn:?H; [| inv H].
(* Goal: and (@eq Z (co_sizeof c0) (co_sizeof c)) (@eq Z (align_attr a (co_alignof c0)) (align_attr a (co_alignof c))) *)
      rewrite (co_consistent_sizeof (@cenv_cs cs_to) c (@cenv_consistent cs_to _ _ H0)).
(* Goal: and (@eq Z (co_sizeof c0) (align (sizeof_composite (@cenv_cs cs_to) (co_su c) (co_members c)) (co_alignof c))) (@eq Z (align_attr a (co_alignof c0)) (align_attr a (co_alignof c))) *)
      rewrite (co_consistent_sizeof (@cenv_cs cs_from) c0 (@cenv_consistent cs_from _ _ H2)).
(* Goal: and (@eq Z (align (sizeof_composite (@cenv_cs cs_from) (co_su c0) (co_members c0)) (co_alignof c0)) (align (sizeof_composite (@cenv_cs cs_to) (co_su c) (co_members c)) (co_alignof c))) (@eq Z (align_attr a (co_alignof c0)) (align_attr a (co_alignof c))) *)
      rewrite (co_consistent_alignof (@cenv_cs cs_to) c (@cenv_consistent cs_to _ _ H0)).
(* Goal: and (@eq Z (align (sizeof_composite (@cenv_cs cs_from) (co_su c0) (co_members c0)) (co_alignof c0)) (align (sizeof_composite (@cenv_cs cs_to) (co_su c) (co_members c)) (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) (@eq Z (align_attr a (co_alignof c0)) (align_attr a (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) *)
      rewrite (co_consistent_alignof (@cenv_cs cs_from) c0 (@cenv_consistent cs_from _ _ H2)).
(* Goal: @eq bool true (cs_preserve_members cs_from cs_to (@coeq cs_from cs_to CCE) m) *)
      simpl in H.
(* Goal: and (@eq Z (align (sizeof_composite (@cenv_cs cs_from) (co_su c0) (co_members c0)) (align_attr (co_attr c0) (alignof_composite (@cenv_cs cs_from) (co_members c0)))) (align (sizeof_composite (@cenv_cs cs_to) (co_su c) (co_members c)) (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) (@eq Z (align_attr a (align_attr (co_attr c0) (alignof_composite (@cenv_cs cs_from) (co_members c0)))) (align_attr a (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) *)
      rewrite !andb_true_iff in H; destruct H as [[? ?] ?].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_list_spec in H; [| apply eqb_member_spec].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_su_spec in H3.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_attr_spec in H4.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply (coeq_consistent _ _ _ _ _ H0) in H1.
      rewrite H in *; rewrite H4 in  *; rewrite H3 in *; clear c0 H H0 H2 H3 H4.
(* Goal: and (@eq Z (align (sizeof_composite (@cenv_cs cs_from) (co_su c) (co_members c)) (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_from) (co_members c)))) (align (sizeof_composite (@cenv_cs cs_to) (co_su c) (co_members c)) (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) (@eq Z (align_attr a (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_from) (co_members c)))) (align_attr a (align_attr (co_attr c) (alignof_composite (@cenv_cs cs_to) (co_members c))))) *)
      split; [f_equal; [ | f_equal] | f_equal; f_equal].
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      * apply sizeof_composite_change_composite; auto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      * apply alignof_composite_change_composite; auto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      * apply alignof_composite_change_composite; auto.
    - destruct ((coeq cs_from cs_to) ! id) eqn:?H.
      * pose proof proj2 (coeq_complete _ _ id) (ex_intro _ b H1) as [co ?].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
        congruence.
      * inv H.
Qed.

Lemma sizeof_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  @sizeof (@cenv_cs cs_from) t = @sizeof (@cenv_cs cs_to) t.
Proof.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  intros.
(* Goal: @eq Z (@sizeof (@cenv_cs cs_from) t) (@sizeof (@cenv_cs cs_to) t) *)
  exact (proj1 (sizeof_alignof_change_composite t H)).
Qed.

Lemma alignof_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  @alignof (@cenv_cs cs_from) t = @alignof (@cenv_cs cs_to) t.
Proof.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  intros.
(* Goal: @eq Z (@alignof (@cenv_cs cs_from) t) (@alignof (@cenv_cs cs_to) t) *)
  exact (proj2 (sizeof_alignof_change_composite t H)).
Qed.

Lemma complete_legal_cosu_type_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  @complete_legal_cosu_type (@cenv_cs cs_from) t = @complete_legal_cosu_type (@cenv_cs cs_to) t.
Proof.
(* Goal: forall (t : type) (_ : @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) t) true) (ofs : Z), iff (align_compatible_rec (@cenv_cs cs_from) t ofs) (align_compatible_rec (@cenv_cs cs_to) t ofs) *)
  intros t.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  type_induction t (@cenv_cs cs_to) (@cenv_consistent cs_to); intros.
  + split; reflexivity.
  + split; reflexivity.
  + split; reflexivity.
  + split; reflexivity.
  + split; reflexivity.
  + simpl.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    apply IH; auto.
  + split; reflexivity.
  + simpl in *.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    unfold test_aux in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    destruct ((@cenv_cs cs_to) ! id) eqn:?H.
    - pose proof proj1 (coeq_complete _ _ _) (ex_intro _ _ H0) as [b ?H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      rewrite H1 in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct b; [| inv H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct ((@cenv_cs cs_from) ! id) eqn:?H; [| inv H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      rewrite !andb_true_iff in H. destruct H as [_ [[? ?] ?]].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_su_spec in H3.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      rewrite H3; auto.
    - destruct ((coeq cs_from cs_to) ! id) eqn:?H.
      * pose proof proj2 (coeq_complete _ _ id) (ex_intro _ b H1) as [co ?].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
        congruence.
      * inv H.
  + simpl in *.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    unfold test_aux in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    destruct ((@cenv_cs cs_to) ! id) eqn:?H.
    - pose proof proj1 (coeq_complete _ _ _) (ex_intro _ _ H0) as [b ?H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      rewrite H1 in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct b; [| inv H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct ((@cenv_cs cs_from) ! id) eqn:?H; [| inv H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      rewrite !andb_true_iff in H. destruct H as [_ [[? ?] ?]].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_su_spec in H3.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      rewrite H3; auto.
    - destruct ((coeq cs_from cs_to) ! id) eqn:?H.
      * pose proof proj2 (coeq_complete _ _ id) (ex_intro _ b H1) as [co ?].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
        congruence.
      * inv H.
Qed.

Lemma field_offset_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall i m,
  true = cs_preserve_members cs_from cs_to (coeq cs_from cs_to) m ->
  field_offset (@cenv_cs cs_from) i m = field_offset (@cenv_cs cs_to) i m.
Proof.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  intros.
(* Goal: @eq (Errors.res Z) (field_offset (@cenv_cs cs_from) i m) (field_offset (@cenv_cs cs_to) i m) *)
  unfold field_offset.
(* Goal: @eq (Errors.res Z) (field_offset_rec (@cenv_cs cs_from) i m Z0) (field_offset_rec (@cenv_cs cs_to) i m Z0) *)
  generalize 0.
(* Goal: @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type (@pair ident type i0 t))) true *)
  symmetry in H.
(* Goal: forall z : Z, @eq (Errors.res Z) (field_offset_rec (@cenv_cs cs_from) i m z) (field_offset_rec (@cenv_cs cs_to) i m z) *)
  induction m as [| [i0 t0] m]; [auto |].
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  intros.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
  simpl in *.
(* Goal: @eq bool (cs_preserve_members cs_from cs_to (@coeq cs_from cs_to CCE) m) true *)
  rewrite andb_true_iff in H.
(* Goal: @eq (Errors.res Z) (if ident_eq i i0 then @Errors.OK Z (align z (@alignof (@cenv_cs cs_from) t0)) else field_offset_rec (@cenv_cs cs_from) i m (Z.add (align z (@alignof (@cenv_cs cs_from) t0)) (@sizeof (@cenv_cs cs_from) t0))) (if ident_eq i i0 then @Errors.OK Z (align z (@alignof (@cenv_cs cs_to) t0)) else field_offset_rec (@cenv_cs cs_to) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0))) *)
  destruct H.
(* Goal: @eq (Errors.res Z) (if ident_eq i i0 then @Errors.OK Z (align z (@alignof (@cenv_cs cs_from) t0)) else field_offset_rec (@cenv_cs cs_from) i m (Z.add (align z (@alignof (@cenv_cs cs_from) t0)) (@sizeof (@cenv_cs cs_from) t0))) (if ident_eq i i0 then @Errors.OK Z (align z (@alignof (@cenv_cs cs_to) t0)) else field_offset_rec (@cenv_cs cs_to) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0))) *)
  if_tac.
  + subst.
(* Goal: @eq Z (align z (@alignof (@cenv_cs cs_from) t0)) (align z (@alignof (@cenv_cs cs_to) t0)) *)
    f_equal.
(* Goal: @eq Z (align z (@alignof (@cenv_cs cs_from) t0)) (align z (@alignof (@cenv_cs cs_to) t0)) *)
    f_equal.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    apply alignof_change_composite; auto.
  + rewrite alignof_change_composite by auto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    rewrite sizeof_change_composite by auto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    apply IHm; auto.
Qed.

Lemma align_compatible_rec_field_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall (m: members),
  true = cs_preserve_members cs_from cs_to (coeq cs_from cs_to) m ->
  Forall
    (Basics.compose
       (fun t : type =>
          cs_preserve_type cs_from cs_to (coeq cs_from cs_to) t = true ->
          forall ofs : Z, @align_compatible_rec (@cenv_cs cs_from) t ofs <-> @align_compatible_rec (@cenv_cs cs_to) t ofs) snd)
    m ->
  forall i t,
    field_type i m = Errors.OK t ->
    forall ofs : Z, @align_compatible_rec (@cenv_cs cs_from) t ofs <-> @align_compatible_rec (@cenv_cs cs_to) t ofs.
Proof.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  intros.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) t ofs) (align_compatible_rec (@cenv_cs cs_to) t ofs) *)
  induction H0 as [| [i0 t0] m]; [inv H1 |].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) t ofs) (align_compatible_rec (@cenv_cs cs_to) t ofs) *)
  simpl in H1.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) t ofs) (align_compatible_rec (@cenv_cs cs_to) t ofs) *)
  if_tac in H1.
  + subst.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) t ofs) (align_compatible_rec (@cenv_cs cs_to) t ofs) *)
    inv H1.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) t ofs) (align_compatible_rec (@cenv_cs cs_to) t ofs) *)
    apply H0.
(* Goal: @eq bool true (cs_preserve_members cs_from cs_to (@coeq cs_from cs_to CCE) m) *)
    simpl in H.
(* Goal: @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type (@pair ident type i0 t))) true *)
    symmetry in H.
(* Goal: @eq bool (cs_preserve_members cs_from cs_to (@coeq cs_from cs_to CCE) m) true *)
    rewrite andb_true_iff in H.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    tauto.
  + apply IHForall; auto.
(* Goal: @eq bool true (cs_preserve_members cs_from cs_to (@coeq cs_from cs_to CCE) m) *)
    simpl in H.
    symmetry in H |- *.
(* Goal: @eq bool (cs_preserve_members cs_from cs_to (@coeq cs_from cs_to CCE) m) true *)
    rewrite andb_true_iff in H.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    tauto.
Qed.

Lemma align_compatible_rec_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  (forall ofs, @align_compatible_rec (@cenv_cs cs_from) t ofs <-> @align_compatible_rec (@cenv_cs cs_to) t ofs).
Proof.
(* Goal: forall (t : type) (_ : @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) t) true) (ofs : Z), iff (align_compatible_rec (@cenv_cs cs_from) t ofs) (align_compatible_rec (@cenv_cs cs_to) t ofs) *)
  intros t.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
  type_induction t (@cenv_cs cs_to) (@cenv_consistent cs_to); intros.
  + split; intros;
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    inv H0; econstructor; eauto.
  + split; intros;
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    inv H0; econstructor; eauto.
  + split; intros;
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    inv H0; econstructor; eauto.
  + split; intros;
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    inv H0; econstructor; eauto.
  + split; intros;
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    inv H0; econstructor; eauto.
  + simpl.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
    split; intros.
    - inv H0.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) t ofs) (align_compatible_rec (@cenv_cs cs_to) t ofs) *)
      1: inv H1.
(* Goal: align_compatible_rec (@cenv_cs cs_from) (Tarray t z a) ofs *)
      constructor.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
      intros.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      apply IH; auto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      rewrite <- sizeof_change_composite by auto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      apply (H5 i); auto.
    - inv H0.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) t ofs) (align_compatible_rec (@cenv_cs cs_to) t ofs) *)
      1: inv H1.
(* Goal: align_compatible_rec (@cenv_cs cs_from) (Tarray t z a) ofs *)
      constructor.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
      intros.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      apply IH; auto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      rewrite sizeof_change_composite by auto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
      apply (H5 i); auto.
  + split; intros;
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
    inv H0; econstructor; eauto.
  + simpl in *.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    unfold test_aux in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    destruct ((@cenv_cs cs_to) ! id) eqn:?H.
    - pose proof proj1 (coeq_complete _ _ _) (ex_intro _ _ H0) as [b ?H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      rewrite H1 in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct b; [| inv H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct ((@cenv_cs cs_from) ! id) eqn:?H; [| inv H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      rewrite !andb_true_iff in H. destruct H as [_ [[? ?] ?]].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_list_spec in H; [| apply eqb_member_spec].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_su_spec in H3.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_attr_spec in H4.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply (coeq_consistent _ _ _ _ _ H0) in H1.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      pose proof align_compatible_rec_field_change_composite _ H1 IH.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tstruct id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tstruct id a) ofs) *)
      pose proof fun i => field_offset_change_composite i _ H1.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
      split; intros.
      * inv H7.
(* Goal: align_compatible_rec (@cenv_cs cs_from) (Tstruct id a) ofs *)
(* Goal: align_compatible_rec (@cenv_cs cs_from) (Tstruct id a) ofs *)
        1: inv H8.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        eapply align_compatible_rec_Tstruct; eauto.
(* Goal: forall (i0 : ident) (t0 : type) (z0 : Z) (_ : @eq (Errors.res type) (field_type i0 (co_members c)) (@Errors.OK type t0)) (_ : @eq (Errors.res Z) (field_offset (@cenv_cs cs_to) i0 (co_members c)) (@Errors.OK Z z0)), align_compatible_rec (@cenv_cs cs_to) t0 (Z.add ofs z0) *)
        rewrite H2 in H10; inv H10.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
        intros.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        rewrite <- H5 by eauto.
        rewrite <- H in H7, H8.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        eapply H12; eauto.
        rewrite <- H8, H.
(* Goal: @eq (Errors.res Z) (field_offset (@cenv_cs cs_from) i0 (co_members co)) (field_offset (@cenv_cs cs_to) i0 (co_members co)) *)
        apply H6.
      * inv H7.
(* Goal: align_compatible_rec (@cenv_cs cs_from) (Tstruct id a) ofs *)
(* Goal: align_compatible_rec (@cenv_cs cs_from) (Tstruct id a) ofs *)
        1: inv H8.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        eapply align_compatible_rec_Tstruct; eauto.
(* Goal: forall (i0 : ident) (t0 : type) (z0 : Z) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)) (_ : @eq (Errors.res Z) (field_offset (@cenv_cs cs_from) i0 (co_members c0)) (@Errors.OK Z z0)), align_compatible_rec (@cenv_cs cs_from) t0 (Z.add ofs z0) *)
        rewrite H0 in H10; inv H10.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
        intros.
(* Goal: align_compatible_rec (@cenv_cs cs_from) t0 (Z.add ofs z0) *)
        rewrite H in H7, H8.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        rewrite H5 by eauto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        eapply H12; eauto.
        rewrite <- H8.
(* Goal: @eq (Errors.res Z) (field_offset (@cenv_cs cs_to) i0 (co_members co)) (field_offset (@cenv_cs cs_from) i0 (co_members co)) *)
        symmetry.
(* Goal: @eq (Errors.res Z) (field_offset (@cenv_cs cs_from) i0 (co_members co)) (field_offset (@cenv_cs cs_to) i0 (co_members co)) *)
        apply H6.
    - destruct ((coeq cs_from cs_to) ! id) eqn:?H.
      * pose proof proj2 (coeq_complete _ _ id) (ex_intro _ b H1) as [co ?].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
        congruence.
      * inv H.
  + simpl in *.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    unfold test_aux in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
    destruct ((@cenv_cs cs_to) ! id) eqn:?H.
    - pose proof proj1 (coeq_complete _ _ _) (ex_intro _ _ H0) as [b ?H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      rewrite H1 in H.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct b; [| inv H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      destruct ((@cenv_cs cs_from) ! id) eqn:?H; [| inv H].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      rewrite !andb_true_iff in H. destruct H as [_ [[? ?] ?]].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_list_spec in H; [| apply eqb_member_spec].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_su_spec in H3.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply eqb_attr_spec in H4.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      apply (coeq_consistent _ _ _ _ _ H0) in H1.
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
      pose proof align_compatible_rec_field_change_composite _ H1 IH.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
      split; intros.
      * inv H6.
(* Goal: align_compatible_rec (@cenv_cs cs_from) (Tstruct id a) ofs *)
        1: inv H7.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        eapply align_compatible_rec_Tunion; eauto.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_to) t0 ofs *)
        rewrite H2 in H9; inv H9.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
        intros.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        rewrite <- H5 by eauto.
        rewrite <- H in H6.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        eapply H11; eauto.
      * inv H6.
(* Goal: align_compatible_rec (@cenv_cs cs_from) (Tstruct id a) ofs *)
        1: inv H7.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        eapply align_compatible_rec_Tunion; eauto.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
        rewrite H0 in H9; inv H9.
(* Goal: forall (i0 : ident) (t0 : type) (_ : @eq (Errors.res type) (field_type i0 (co_members c0)) (@Errors.OK type t0)), align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
        intros.
(* Goal: align_compatible_rec (@cenv_cs cs_from) t0 ofs *)
        rewrite H in H6.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        rewrite H5 by eauto.
(* Goal: iff (@ex composite (fun co : composite => @eq (option composite) (@PTree.get composite i (@cenv_cs cs_to)) (@Some composite co))) (@ex bool (fun b : bool => @eq (option bool) (@PTree.get bool i cs_preserve_env) (@Some bool b))) *)
        eapply H11; eauto.
    - destruct ((coeq cs_from cs_to) ! id) eqn:?H.
      * pose proof proj2 (coeq_complete _ _ id) (ex_intro _ b H1) as [co ?].
(* Goal: iff (align_compatible_rec (@cenv_cs cs_from) (Tunion id a) ofs) (align_compatible_rec (@cenv_cs cs_to) (Tunion id a) ofs) *)
        congruence.
      * inv H.
Qed.
