Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Natmap.
Require Import FMaps.
Require Import EqNat.
Require Import lj.
Require Import FMapFacts.
Require Import Natmap.
Require Import Classical.
Require Import base2.
Require Import Max.
Require Import lj_sound.
Require Import lj_constr_sound.

Inductive rmb : Set :=
  rmb_def : Ss -> Ss -> x -> rmb.

Inductive rmd : Set :=
  rmd_def : ms -> rmb -> rmd.

Inductive rcld : Set := 
  refines_cld_def : dcl -> cl -> fds -> list md -> list rmd -> rcld.

Inductive F : Set :=
  feature_def : list rcld -> list cld -> F.

Definition PS : Set := list F.

Definition cons_option (A : Type) (a : A) (l : option (list A)) : option (list A) :=
  match l with
    Some l' => Some (a :: l')
    | _ => None
  end.
           
Implicit Arguments cons_option [A].

Fixpoint vd_list_eq (vd_list1 vd_list2 : list vd) {struct vd_list1}: bool :=
  match vd_list1, vd_list2 with
    (vd_def (ty_def cl1) var1) :: vd_list1', (vd_def (ty_def cl2) var2) :: vd_list2' => 
    if (eq_nat_dec var1 var2) then cl_eq cl1 cl2 && (vd_list_eq vd_list1' vd_list2') else false
    | nil, nil => true
    | _, _ => false
  end.

Definition ms_eq (ms1 ms2 : ms) : bool :=
  match ms1, ms2 with
    ms_def (ty_def cl1) m1 list_vd1, ms_def (ty_def cl2) m2 list_vd2 =>
    if (eq_nat_dec m1 m2) then
      (cl_eq cl1 cl2) && (vd_list_eq list_vd1 list_vd2) 
      else false
  end.

Fixpoint compose_refined_md (mds : list md) (rmd : rmd) {struct mds}: option (list md) :=
  match mds, rmd with
    cons (md_def ms' (mb_def Ss' x')) mds', rmd_def ms'' (rmb_def before_s after_s y) => 
    if (ms_eq ms' ms'') then
      Some (cons (md_def ms' (mb_def (before_s ++ Ss' ++ after_s) y)) mds')
      else cons_option (md_def ms' (mb_def Ss' x')) (compose_refined_md mds' rmd) 
    | nil, _ => None
  end.
  
Fixpoint introduce_field (fds' : list fd) (fd' : fd) {struct fds'} : list fd :=
  match fds', fd' with
    (fd_def (ty_def cl') f') :: fds'', fd_def (ty_def cl'') f'' =>
    if (eq_nat_dec f' f'') then 
      if (cl_eq cl' cl'') then fds'
        else (fd_def (ty_def cl') f') :: (introduce_field fds'' fd')
      else (fd_def (ty_def cl') f') :: (introduce_field fds'' fd')
    | _, _ => fd' :: nil
  end.

Fixpoint introduce_method (mds' : list md) (md' : md) {struct mds'} : list md :=
  match mds', md' with
    (md_def ms' mb') :: mds'', md_def ms'' mb'' => 
    if (ms_eq ms' ms'') then md' :: mds''
      else (md_def ms' mb') :: (introduce_method mds'' md')
    | _, _ => md' :: nil
  end.

Fixpoint rm_dcl (cld_list : list cld) (cld' : cld) {struct cld_list} : list cld :=
  match cld_list, cld' with
    (cld_def dcl'' cl' fds' mds) :: cld_list', cld_def dcl' _ _ _ => 
    if (eq_nat_dec dcl' dcl'') then rm_dcl cld_list' cld' 
      else (cld_def dcl'' cl' fds' mds) :: (rm_dcl cld_list' cld')
    | _, _ => nil
  end.
    
Fixpoint introduce_class (cld_list : list cld) (cld' : cld) {struct cld_list} : list cld :=
  match cld_list, cld' with
    (cld_def dcl' cl' fds mds) :: cld_list', cld_def dcl'' cl'' fds' mds' => 
    if (eq_nat_dec dcl' dcl'') then cld' :: cld_list'
      else (cld_def dcl' cl' fds mds) :: (introduce_class cld_list' cld')
    | _, _ => cld' :: nil
  end.

Definition introduce_fields (fds' fds'' : list fd) : list fd :=
  fold_right (fun (fd' : fd) (lfd : list fd) => introduce_field lfd fd') fds' fds''.

Definition introduce_methods (mds' mds'' : list md) : list md :=
  fold_right (fun (md' : md) (lmd : list md) => introduce_method lmd md') mds' mds''.

Definition introduce_classes (cld_list' cld_list'' : list cld) : list cld :=
  fold_right (fun (cld' : cld) (list_cld : list cld) => cld' :: (rm_dcl list_cld cld')) cld_list' cld_list''.

Definition compose_refined_mds (mds' : list md) (rmds : list rmd) : option (list md) :=
  fold_right (fun (rmd' : rmd) (lmd : option (list md)) => 
    match lmd with
      Some lmd' => compose_refined_md lmd' rmd'
      | None => None
    end) (Some mds') rmds.

Fixpoint compose_refines_class (p : P) (rcld' : rcld) {struct p}: option P :=
  match p, rcld' with 
    cons (cld_def dcl' cl' fds' mds') p', refines_cld_def dcl'' cl'' fds'' mds'' rmds =>
    if (eq_nat_dec dcl' dcl'') then
      match compose_refined_mds mds' rmds with
        Some mds''' =>
        Some (cons (cld_def dcl' cl'' (introduce_fields fds' fds'') (introduce_methods mds''' mds'') ) p')
        | None => None
      end
      else cons_option (cld_def dcl' cl' fds' mds') (compose_refines_class p' rcld')
    | _, _ => None
  end.

Definition compose (p : P) (f' : F) : option P :=
  match f' with 
    feature_def rclds clds =>
    match (fold_right (fun (rcld' : rcld) (op : option P) => 
      match op with
        Some p' => compose_refines_class p' rcld'
        | None => None
      end) (Some p) rclds) with
    Some p' => Some (introduce_classes p' clds)
      | None => None
    end
  end.

Fixpoint compose_all (ps : PS) : option P :=
  match ps with
    f' :: ps' => match compose_all ps' with
                   Some p => compose p f'
                   | None => None
                 end
    | nil => Some nil
  end.

Inductive comp_constraint : Set :=
  introduced_method_constr : ms -> dcl -> comp_constraint
  | introduced_class_constr : dcl -> comp_constraint. 

Fixpoint gen_meth_comp_constr (rmds : list rmd) (dcl' : dcl) {struct rmds} : list comp_constraint :=
  match rmds with 
    (rmd_def ms' _) :: rmds' => (introduced_method_constr ms' dcl') :: gen_meth_comp_constr rmds' dcl'
    | nil => nil
  end.

Fixpoint gen_cld_comp_constr (rclds : list rcld) {struct rclds} : list comp_constraint :=
  match rclds with 
    (refines_cld_def dcl' cl' _ _ rmds) :: rclds' => 
    (introduced_class_constr dcl') :: ((gen_meth_comp_constr rmds dcl') ++ (gen_cld_comp_constr rclds'))
    | nil => nil
  end.

Fixpoint gen_comp_constr (ps : PS) : list comp_constraint := 
  match ps with 
    (feature_def rclds _) :: ps' => (gen_cld_comp_constr rclds) ++ gen_comp_constr ps'
    | nil => nil
  end.

Fixpoint meth_in_mds (mds : list md) (ms' : ms) {struct mds} : bool :=
  match mds with 
    (md_def ms'' _ ) :: mds' => if (ms_eq ms' ms'') then true else meth_in_mds mds' ms'
    | nil => false
  end.

Fixpoint sat_meth_constr_rclds (rclds : list rcld) (dcl' : dcl) (ms' : ms) {struct rclds} : bool :=
  match rclds with
    (refines_cld_def dcl'' _ _ mds' _) :: rclds'=> if (eq_nat_dec dcl' dcl'') then if (meth_in_mds mds' ms') then
      true else sat_meth_constr_rclds rclds' dcl' ms' else  sat_meth_constr_rclds rclds' dcl' ms'
    | nil => false
  end.

Definition sat_meth_constr_clds (clds : list cld) (dcl' : dcl) (ms' : ms) : bool :=
  match head (path clds (cl_dcl dcl')) with 
    Some (cld_def _ _ _ mds') => meth_in_mds mds' ms'
    | None => false
  end.
    
Fixpoint sat_meth_constr_ps (dcl' : dcl) (ms' : ms) (ps : PS) {struct ps}: bool :=
  match ps with 
    (feature_def rclds clds) :: ps' => if (in_path clds dcl') then sat_meth_constr_clds clds dcl' ms' else
      if sat_meth_constr_rclds rclds dcl' ms' then true else
        sat_meth_constr_ps dcl' ms' ps'
    | nil => false
  end.

Definition sat_meth_constr_p (dcl' : dcl) (ms' : ms) (p : P) : bool :=
  match head (path p (cl_dcl dcl')) with 
    Some (cld_def _ _ _ mds') => meth_in_mds mds' ms'
    | None => false
  end.

Definition in_clds (dcl' : dcl) (clds : list cld) : bool := 
  match head (path clds (cl_dcl dcl')) with
    Some (cld_def _ _ _ _) => true
    | None => false
  end.

Fixpoint sat_cld_constr_ps (dcl' : dcl) (ps : PS) {struct ps} : bool :=
  match ps with 
    (feature_def _ clds) :: ps' => if (in_clds dcl' clds) then true
      else sat_cld_constr_ps dcl' ps'
    | nil => false
  end.    

Fixpoint sat_comp_constr_ps (c_list : list comp_constraint) (ps: PS) : bool :=
  match c_list with
    (introduced_method_constr ms' dcl') :: c_list' => sat_meth_constr_ps dcl' ms' ps && (sat_comp_constr_ps c_list' ps)
    | (introduced_class_constr dcl') :: c_list' => sat_cld_constr_ps dcl' ps && (sat_comp_constr_ps c_list' ps)
    | nil => true
  end.
    
Fixpoint sat_comp_constr_p (c_list : list comp_constraint) (p : P) : bool :=
  match c_list with
    (introduced_method_constr ms' dcl') :: c_list' => sat_meth_constr_p dcl' ms' p && (sat_comp_constr_p c_list' p)
    | (introduced_class_constr dcl') :: c_list' => in_clds dcl' p && (sat_comp_constr_p c_list' p)
    | nil => true
  end.

Fixpoint sat_meth_constr_rclds' (dcl' : dcl) (ms' : ms) (rclds' : list rcld) (p : P) {struct rclds'}: bool :=
  match rclds' with
  (refines_cld_def dcl'' _ _ mds' _) :: rclds'' =>  if (eq_nat_dec dcl' dcl'') then
    if meth_in_mds mds' ms' then true else sat_meth_constr_rclds' dcl' ms' rclds'' p
    else sat_meth_constr_rclds' dcl' ms' rclds'' p
  | nil => sat_meth_constr_p dcl' ms' p
  end.

Fixpoint sat_comp_constr_rclds (c_list : list comp_constraint) (rclds : list rcld) (p : P) {struct c_list} : bool :=
  match c_list with
    (introduced_method_constr ms' dcl') :: c_list' => sat_meth_constr_rclds' dcl' ms' rclds p && 
    (sat_comp_constr_rclds c_list' rclds p)
    | (introduced_class_constr dcl') :: c_list' => in_clds dcl' p && (sat_comp_constr_rclds c_list' rclds p)
    | nil => true
  end.
      
Fixpoint sat_meth_constr_rclds_ps (dcl' : dcl) (ms' : ms) (rclds' : list rcld) (ps : PS) {struct rclds'}: bool :=
  match rclds' with
  (refines_cld_def dcl'' _ _ mds' _) :: rclds'' =>  if (eq_nat_dec dcl' dcl'') then
    if meth_in_mds mds' ms' then true else sat_meth_constr_rclds_ps dcl' ms' rclds'' ps
    else sat_meth_constr_rclds_ps dcl' ms' rclds'' ps
  | nil => sat_meth_constr_ps dcl' ms' ps
  end.

Fixpoint sat_comp_constr_rclds_ps (c_list : list comp_constraint) (rclds : list rcld) (ps : PS) {struct c_list} : bool :=
  match c_list with
    (introduced_method_constr ms' dcl') :: c_list' => sat_meth_constr_rclds_ps dcl' ms' rclds ps && 
    (sat_comp_constr_rclds_ps c_list' rclds ps)
    | (introduced_class_constr dcl') :: c_list' => sat_cld_constr_ps dcl' ps && (sat_comp_constr_rclds_ps c_list' rclds ps)
    | nil => true
  end.

Fixpoint safe_compose_rclds (rclds : list rcld) (p : P) : bool :=
  match rclds with
    (refines_cld_def dcl' _ _ _ rmds') :: rclds' => in_clds dcl' p &&
    sat_comp_constr_rclds (gen_meth_comp_constr rmds' dcl') rclds' p && safe_compose_rclds rclds' p
    | nil => true
  end.

Fixpoint safe_compose_rclds_ps (rclds : list rcld) (ps : PS) : bool :=
  match rclds with
    (refines_cld_def dcl' _ _ _ rmds') :: rclds' => sat_cld_constr_ps dcl' ps &&
    sat_comp_constr_rclds_ps (gen_meth_comp_constr rmds' dcl') rclds' ps && safe_compose_rclds_ps rclds' ps
    | nil => true
  end.

Fixpoint safe_compose (ps : PS) : bool :=
  match ps with 
    (feature_def rclds clds) :: ps' => safe_compose_rclds_ps rclds ps' && safe_compose ps'
    | _ => true
  end.

Lemma eq_vd_list_eq : forall (vd_list1 vd_list2 : list vd), 
  vd_list_eq vd_list1 vd_list2 = true <-> vd_list1 = vd_list2.
  induction vd_list1; destruct vd_list2; pa; intros; auto.
  simpl in H; discriminate.
  discriminate.
  simpl in H; destruct a; destruct t; discriminate.
  discriminate.
  simpl in H; destruct a; destruct v; destruct t; destruct t0.
  generalize H; clear H; case (eq_nat_dec v0 v); intros.
  destruct (andb_prop _ _ H).
  rewrite ((proj1 (eq_cl_eq _ _)) H0).
  rewrite ((proj1 (IHvd_list1 _)) H1).
  congruence.
  discriminate.
  inversion H; subst.
  simpl; destruct v; destruct t; case (eq_nat_dec v v); intros.
  apply andb_true_intro; pa.
  destruct c; simpl. 
  case (eq_nat_dec d d); intros; auto.
  auto.
  applyI IHvd_list1.
  congruence.
Qed.

Lemma eq_ms_eq : forall (ms1 ms2 : ms), ms_eq ms1 ms2 = true <-> ms1 = ms2.
  destruct ms1; destruct ms2; destruct t; destruct t0; simpl;
    case (eq_nat_dec m m0); pa; intros.
  destruct (andb_prop _ _ H).
  rewrite ((proj1 (eq_cl_eq _ _)) H0).
  rewrite ((proj1 (eq_vd_list_eq _ _)) H1); congruence.
  inversion H; subst; apply andb_true_intro; pa.
  applyI eq_cl_eq; auto.
  applyI eq_vd_list_eq; auto.
  discriminate.
  congruence.
Qed.

Lemma sat_comp_constr_app_ps : forall (c_list1 c_list2 : list comp_constraint) (ps : PS), 
  (sat_comp_constr_ps (c_list1 ++ c_list2) ps = true) <-> (sat_comp_constr_ps c_list1 ps = true /\ 
    sat_comp_constr_ps c_list2 ps = true).
  induction c_list1; simpl; pa; intros.
  pa; simpl; auto.
  bd H.
  destruct a; pa.
  destruct (andb_prop _ _ H); apply andb_true_intro; pa.
  exact (proj1 ((proj1 (IHc_list1 _ _)) H1)).
  destruct (andb_prop _ _ H); exact (proj2 ((proj1 (IHc_list1 _ _)) H1)).
  destruct (andb_prop _ _ H); apply andb_true_intro; pa.
  exact (proj1 ((proj1 (IHc_list1 _ _)) H1)).
  destruct (andb_prop _ _ H); exact (proj2 ((proj1 (IHc_list1 _ _)) H1)).
  destruct a; bd H.
  destruct (andb_prop _ _ H2); apply andb_true_intro; pa.
  applyI IHc_list1; pa.
  destruct (andb_prop _ _ H2); apply andb_true_intro; pa.
  applyI IHc_list1; pa.
Qed.

Lemma sat_comp_constr_app_p : forall (c_list1 c_list2 : list comp_constraint) (p : P), 
  (sat_comp_constr_p (c_list1 ++ c_list2) p = true) <-> (sat_comp_constr_p c_list1 p = true /\ 
    sat_comp_constr_p c_list2 p = true).
  induction c_list1; simpl; pa; intros.
  pa; simpl; auto.
  bd H.
  destruct a; pa.
  destruct (andb_prop _ _ H); apply andb_true_intro; pa.
  exact (proj1 ((proj1 (IHc_list1 _ _)) H1)).
  destruct (andb_prop _ _ H); exact (proj2 ((proj1 (IHc_list1 _ _)) H1)).
  destruct (andb_prop _ _ H); apply andb_true_intro; pa.
  exact (proj1 ((proj1 (IHc_list1 _ _)) H1)).
  destruct (andb_prop _ _ H); exact (proj2 ((proj1 (IHc_list1 _ _)) H1)).
  destruct a; bd H.
  destruct (andb_prop _ _ H2); apply andb_true_intro; pa.
  applyI IHc_list1; pa.
  destruct (andb_prop _ _ H2); apply andb_true_intro; pa.
  applyI IHc_list1; pa.
Qed.

Lemma sat_comp_constr_app_rclds : forall (c_list1 c_list2 : list comp_constraint) (rclds : list rcld) (p :P), 
  (sat_comp_constr_rclds (c_list1 ++ c_list2) rclds p = true) <-> 
  (sat_comp_constr_rclds c_list1 rclds p = true /\ sat_comp_constr_rclds c_list2 rclds p = true).
  induction c_list1; simpl; pa; intros.
  pa; simpl; auto.
  bd H.
  destruct a; pa.
  destruct (andb_prop _ _ H); apply andb_true_intro; pa.
  exact (proj1 ((proj1 (IHc_list1 _ _ _ )) H1)).
  destruct (andb_prop _ _ H); exact (proj2 ((proj1 (IHc_list1 _ _ _)) H1)).
  destruct (andb_prop _ _ H); apply andb_true_intro; pa.
  exact (proj1 ((proj1 (IHc_list1 _ _ _)) H1)).
  destruct (andb_prop _ _ H); exact (proj2 ((proj1 (IHc_list1 _ _ _)) H1)).
  destruct a; bd H.
  destruct (andb_prop _ _ H2); apply andb_true_intro; pa.
  applyI IHc_list1; pa.
  destruct (andb_prop _ _ H2); apply andb_true_intro; pa.
  applyI IHc_list1; pa.
Qed.

Lemma cons_option_Some : forall  (A : Type) (a : A) (l : option (list A)) (la : list A),
  cons_option a l = Some la -> exists la', l = Some la'.
  intros A a l; case l; intros.
  exists l0; reflexivity.
  simpl in H; discriminate.
Qed.

Lemma In_mds_In_compose : forall (mds mds' : list md) (rmb' : rmb) (ms' ms'': ms) (mb' : mb),
  compose_refined_md mds (rmd_def ms' rmb') = Some mds' ->
  In (md_def ms'' mb') mds -> exists mb'', In (md_def ms'' mb'') mds'.
  induction mds; simpl; intros.
  discriminate.
  bd H0.
  subst; destruct mb'; destruct rmb'.
  caseEq (ms_eq ms'' ms'); intros H0; rewrite H0 in H.
  inversion H.
  exists (mb_def (s0 ++ s ++ s1) x0); simpl; po1;
    rewrite ((proj1 (eq_ms_eq ms'' ms')) H0); reflexivity.
  destruct (cons_option_Some _ _ _ _ H); unfold cons_option in H; rewrite H1 in H; inversion H.
  exists (mb_def s x); simpl; po1.
   destruct a; destruct m0; destruct rmb'.
  caseEq (ms_eq m ms'); intros H1; rewrite H1 in H.
  inversion H; subst.
  exists mb'; simpl; po2.
  destruct (cons_option_Some _ _ _ _ H); unfold cons_option in H; rewrite H2 in H; inversion H.
  destruct (IHmds _ _ _ _ _ H2 H0).
  exists x2; simpl; po2.
Qed.

Lemma In_compose_In_mds : forall (mds mds' : list md) (rmb' : rmb) (ms' ms'': ms) (mb': mb),
  compose_refined_md mds (rmd_def ms' rmb') = Some mds' ->
   In (md_def ms'' mb') mds' -> exists mb'', In (md_def ms'' mb'') mds.
  induction mds; simpl; intros.
  discriminate.
  bd H0.
  destruct a; destruct m0; destruct rmb'.
  caseEq (ms_eq m ms'); intros H1; rewrite H1 in H.
  inversion H; rewrite <- H3 in H0.
  simpl in H0; bd H0.
  inversion H0.
  exists (mb_def s x); po1.
  exists mb'; po2.
  destruct (cons_option_Some _ _ _ _ H); rewrite H2 in H; simpl in H; inversion H.
  rewrite <- H4 in H0; simpl in H0; bd H0.
  inversion H0.
  exists (mb_def s x); po1.
  destruct (IHmds _ _ _ _ _ H2 H0).
  exists x2; po2.
Qed.

Lemma in_mds_In_mds : forall (mds : list md) (ms' : ms),
  meth_in_mds mds ms' = true -> exists mb', In (md_def ms' mb') mds.
  induction mds; simpl.
  intros; discriminate.
  intro; destruct a; caseEq (ms_eq ms' m); intros.
  exists m0; po1; rewrite ((proj1 (eq_ms_eq _ _ )) H); reflexivity.
  destruct (IHmds _ H0).
  exists x; po2.
Qed.

Lemma In_mds_in_mds : forall (mds : list md) (ms' : ms) (mb' : mb),
   In (md_def ms' mb') mds -> meth_in_mds mds ms' = true.
  induction mds; simpl.
  intros; contradiction.
  intros; bd H.
  rewrite H; caseEq (ms_eq ms' ms'); intros; try reflexivity.
  rewrite (((proj2 (eq_ms_eq _ _ )) (refl_equal ms'))) in H0; discriminate.
  destruct a.
  rewrite (IHmds _ _ H); case (ms_eq ms' m); reflexivity.
Qed.  

Lemma in_rclds_in_p : forall (dcl' : dcl) (cl' : cl) (fds' : fds) (mds : list md) (rmds : list rmd) (p p' : P),
  compose_refines_class p (refines_cld_def dcl' cl' fds' mds rmds) = Some p' ->
  exists fds'', exists mds'', In (cld_def dcl' cl' fds'' mds'') p'.
  induction p; intros.
  simpl in H; discriminate.
  destruct a; simpl in H.
  generalize H; clear H; case (eq_nat_dec d dcl'); intros.
  caseEq (compose_refined_mds l rmds); intros; rewrite H0 in H.
  inversion H.
  exists (introduce_fields f fds'); exists (introduce_methods l0 mds); simpl; rewrite e; po1.
  discriminate.
  unfold cons_option in H; caseEq (compose_refines_class p (refines_cld_def dcl' cl' fds' mds rmds)); 
    intros; rewrite H0 in H.
  inversion H.
  import (IHp _ H0).
  bd H1.
  exists x; exists x0; po2.
  discriminate.
Qed.    

Lemma in_rclds_mds_in_p : forall (dcl' : dcl) (cl' : cl) (fds' : fds) (ms' : ms) (mds : list md) (mb' : mb)
  (rmds : list rmd) (p p' : P), 
  compose_refines_class p (refines_cld_def dcl' cl' fds' mds rmds) = Some p' -> In (md_def ms' mb') mds ->
  exists fds'', exists mds'', In (cld_def dcl' cl' fds'' mds'') p' /\ (exists mb'', In (md_def ms' mb'') mds'').
  induction p; intros.
  simpl in H; discriminate.
  destruct a; simpl in H.
  generalize H; clear H; case (eq_nat_dec d dcl'); intros.
  caseEq (compose_refined_mds l rmds); intros; rewrite H1 in H.
  inversion H.
  exists (introduce_fields f fds'); exists (introduce_methods l0 mds); simpl; rewrite e; pa. 
  po1.
  generalize H0; clear; induction mds.
  simpl; intros; contradiction.
  destruct a; simpl.
  intros; bd H0.
  inversion H0; subst.
  exists mb'.
  clear; induction (introduce_methods l0 mds).
  simpl; po1.
  destruct a; simpl.
  simpl; caseEq (ms_eq m ms'); intros.
  simpl; po1.
  simpl; po2.
  destruct (IHmds H0).
  cs (m = ms'); subst.
  exists m0.
  clear; induction (introduce_methods l0 mds).
  simpl; po1.
  destruct a; simpl.
  simpl; caseEq (ms_eq m ms'); intros.
  simpl; po1.
  simpl; po2.
  simpl; exists x.
  generalize H H1; clear; induction (introduce_methods l0 mds).
  simpl; intros; contradiction.
  destruct a; simpl; intros.
  bd H.
  inversion H; subst.
  simpl; caseEq (ms_eq ms' m); intros.
  rewrite ((proj1 (eq_ms_eq _ _)) H0) in H1.
  congruence.
  simpl; po1.
  case (ms_eq m1 m).
  simpl; po2.
  simpl; po2; auto.
  discriminate.
  destruct (cons_option_Some _ _ _ _ H).
  import (IHp _ H1 H0); bd H2.
  rewrite H1 in H; simpl in H; inversion H.
  exists x0; exists x1; pa.
  simpl; po2.
  exists x2; exact H2.
Qed.

Lemma in_p_in_compose_rcld : forall (dcl' dcl'': dcl) (cl' cl'' : cl) (fds' fds'': fds) (mds' mds'': list md) 
  (rmds : list rmd) (p p' : P), dcl' <> dcl'' -> In (cld_def dcl' cl' fds' mds') p -> 
  compose_refines_class p (refines_cld_def dcl'' cl'' fds'' mds'' rmds) = Some p' ->
  In (cld_def dcl' cl' fds' mds') p'.
  induction p.
  simpl; contradiction.
  destruct a; simpl; case (eq_nat_dec d dcl''); intros.
  bd H0.
  congruence.
  destruct (compose_refined_mds l rmds).
  inversion H1.
  simpl; po2.
  discriminate.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; simpl in H1.
  bd H0.
  inversion H0; subst.
  inversion H1; po1.
  import (IHp _ H H0 H2).
  inversion H1; po2.
Qed.
    
Lemma in_p_in_compose_rcld' : forall (dcl': dcl) (cl' cl'' : cl) (fds' fds'': fds) (mds' mds'': list md) 
  (rmds : list rmd) (p p' : P), In (cld_def dcl' cl' fds' mds') p -> distinct _ (names p) -> 
  compose_refines_class p (refines_cld_def dcl' cl'' fds'' mds'' rmds) = Some p' ->
  exists mds''',  compose_refined_mds mds' rmds = Some mds''' /\ 
    In (cld_def dcl' cl'' (introduce_fields fds' fds'') (introduce_methods mds''' mds'')) p'.
  induction p.
  simpl; contradiction.
  destruct a; simpl; case (eq_nat_dec d dcl'); intros.
  bd H.
  inversion H; subst.
  destruct (compose_refined_mds mds' rmds).
  exists l; pa.
  inversion H1; simpl; po1.
  discriminate.
 caseEq (compose_refined_mds l rmds); intros; rewrite H2 in H1; inversion H1.
 bd H0; subst.
 elimtype False; apply H6; generalize H; clear; induction p.
 simpl; auto.
 simpl; destruct a; intros.
 bd H.
 inversion H; subst; po1.
 simpl; po2; auto.
 bd H.
 congruence.
 bd H0; destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; 
   simpl in H1; inversion H1.
 import (IHp _ H H0 H2).
 bd H3.
 exists x0; pa.
 simpl; po2.
Qed.

Lemma in_compose_rcld_in_p : forall (dcl' dcl'': dcl) (cl' cl'' : cl) (fds' fds'': fds) (mds' mds'': list md) 
  (rmds : list rmd) (p p' : P), dcl' <> dcl'' -> In (cld_def dcl' cl' fds' mds') p' -> 
  compose_refines_class p (refines_cld_def dcl'' cl'' fds'' mds'' rmds) = Some p' ->
  In (cld_def dcl' cl' fds' mds') p.
  induction p.
  simpl; intros; discriminate.
  destruct a; simpl; case (eq_nat_dec d dcl''); intros.
  subst.
  destruct (compose_refined_mds l rmds).
  inversion H1; subst.
  simpl in H0; bd H0. 
  inversion H0.
  congruence.
  simpl; po2.
  discriminate.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; simpl in H1.
  inversion H1; subst; clear H1.
  simpl in H0; bd H0.
  po1.
  import (IHp _ H H0 H2).
  po2.
Qed.

Lemma in_compose_rcld_in_p' : forall (dcl': dcl) (cl' cl'' : cl) (fds1 fds2: fds) (mds1 mds2: list md) 
  (rmds : list rmd) (p p' : P), In (cld_def dcl' cl' fds1 mds1) p' -> distinct _ (names p) -> 
  compose_refines_class p (refines_cld_def dcl' cl'' fds2 mds2 rmds) = Some p' ->
  exists mds', exists mds'', compose_refined_mds mds' rmds = Some mds'' /\ 
    mds1 = (introduce_methods mds'' mds2) /\ exists fds',
    fds1 = introduce_fields fds' fds2 /\ exists cl'', In (cld_def dcl' cl'' fds' mds') p.
  induction p.
  simpl; intros; discriminate.
  destruct a; simpl; case (eq_nat_dec d dcl'); intros.
  bd H0.
  caseEq (compose_refined_mds l rmds); intros; rewrite H2 in H1.
  inversion H1; subst; clear H1.
  simpl in H; bd H.
  inversion H; subst.
  exists l; exists l0; repeat pa.
  exists f; pa.
  exists c; po1.
  elimtype False; apply H4.
  apply (In_names _ _ _ _ _ H).
  discriminate.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; simpl in H1; inversion H1; subst; clear H1.
  simpl in H; bd H.
  congruence.
  bd H0.
  import (IHp _ H H0 H2); bd H1; subst.
  exists x0; exists x1; repeat pa; exists x2; pa; exists x3; po2.
Qed.

Lemma in_mds_in_compose : forall (ms' : ms) (rmds' : list rmd) (mds' mds'' : list md),
  meth_in_mds mds' ms' = true -> compose_refined_mds mds' rmds' = Some mds'' ->
  meth_in_mds mds'' ms' = true.
  induction rmds'.
  simpl; congruence.
  destruct a; simpl.
  intros mds' mds''; caseEq (compose_refined_mds mds' rmds'); intros.
  import (IHrmds' _ _ H0 H); clear IHrmds' H0 H.
  generalize mds'' mds' H1 H2; clear.
  induction l; intros; simpl in H2.
  discriminate.
  destruct a. simpl in H1; destruct m1; destruct r.
  caseEq (ms_eq ms' m0); caseEq (ms_eq m0 m); intros; rewrite H0 in H2; rewrite H in H1.
  inversion H1; simpl.
  rewrite H0; auto.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H3 in H1; simpl in H1; inversion H1.
  simpl; rewrite H0; auto.
  inversion H1; simpl; rewrite H0; exact H2.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H3 in H1; simpl in H1; inversion H1.
  simpl; rewrite H0; auto.
  discriminate.
Qed.  
  
Lemma in_compose_in_mds : forall (ms' : ms) (rmds' : list rmd) (mds' mds'' : list md),
  meth_in_mds mds'' ms' = true -> compose_refined_mds mds' rmds' = Some mds'' ->
  meth_in_mds mds' ms' = true.
  induction rmds'.
  simpl; congruence.
  destruct a; simpl.
  intros mds' mds''; caseEq (compose_refined_mds mds' rmds'); intros.
  apply (IHrmds' mds' l); auto.
  generalize mds'' H0 H1; clear; induction l.
  simpl; intros; discriminate.
  destruct a; simpl; destruct m1; destruct r; caseEq (ms_eq ms' m0); auto;
    caseEq (ms_eq m0 m).
  intros; inversion H2; subst.
  simpl in H1; rewrite H0 in H1; auto.
  intros; destruct (cons_option_Some _ _ _ _ H2); rewrite H3 in H2; simpl in H2; 
    inversion H2; subst; simpl in H1; rewrite H0 in H1.
  apply (IHl _ H1 H3).
  discriminate.
Qed.

Lemma in_mds_in_introduce : forall (ms' : ms) (mds' mds'' : list md),
  meth_in_mds mds' ms' = true -> meth_in_mds (introduce_methods mds' mds'') ms' = true.
  induction mds''; simpl.
  auto.
  intros; generalize (IHmds'' H); clear.
  destruct a; induction (introduce_methods mds' mds'').
  simpl; intros; discriminate.
  destruct a; simpl.
  caseEq (ms_eq ms' m1).
  caseEq (ms_eq m1 m).
  intros H H0 H1; simpl; rewrite ((proj1 (eq_ms_eq _ _ )) H0 ); 
    rewrite ((proj1 (eq_ms_eq _ _ )) H); rewrite ((proj2 (eq_ms_eq m _ )) (refl_equal _)); reflexivity.
  intros H H0 H1; simpl; rewrite H0; reflexivity.
  caseEq (ms_eq m1 m).
  simpl.
  intros H H0 H1; simpl; rewrite <- ((proj1 (eq_ms_eq _ _ )) H); rewrite H0; exact H1.
  intros; simpl; rewrite H0; auto.
Qed.

Lemma in_mds_in_introduce' : forall (ms' : ms) (mds' mds'' : list md),
  meth_in_mds mds'' ms' = true -> meth_in_mds (introduce_methods mds' mds'') ms' = true.
  induction mds''; simpl.
  intros; discriminate.
  destruct a; caseEq (ms_eq ms' m); intros.
  rewrite ((proj1 (eq_ms_eq _ _ )) H); clear; induction (introduce_methods mds' mds'').
  simpl; rewrite ((proj2 (eq_ms_eq m _ )) (refl_equal _)); reflexivity.
  destruct a; simpl.
  caseEq (ms_eq m1 m); intros.
  simpl; rewrite ((proj2 (eq_ms_eq m _ )) (refl_equal _)); reflexivity.
  simpl; case (ms_eq m m1); auto.
  generalize (IHmds'' H0) H; clear.
  induction (introduce_methods mds' mds'').
  simpl; intros; discriminate.
  destruct a; simpl.
  caseEq (ms_eq ms' m1); intros.
  caseEq (ms_eq m1 m); intros.
  rewrite ((proj1 (eq_ms_eq _ _ )) H) in H1; rewrite H2 in H1; discriminate.
  simpl; rewrite H; auto.
  caseEq (ms_eq m1 m); intros.
  simpl; rewrite H1; exact H0.
  simpl; rewrite H; auto.
Qed.
  
Lemma in_introduce_in_mds : forall (ms' : ms) (mds' mds'' : list md),
  meth_in_mds (introduce_methods mds' mds'') ms' = true -> meth_in_mds mds'' ms' = false -> 
  meth_in_mds mds' ms' = true.
  induction mds''; simpl.
  intros; congruence.
  destruct a; caseEq (ms_eq ms' m); intros.
  discriminate.
  apply IHmds''; auto.
  rewrite <- H0; generalize H; clear; induction (introduce_methods mds' mds'').
  simpl.
  intros; rewrite H; auto.
  destruct a; simpl; caseEq (ms_eq m1 m).
  intros H H0; simpl; rewrite ((proj1 (eq_ms_eq _ _ )) H); rewrite H0; auto.
  simpl; caseEq (ms_eq ms' m1); auto.
Qed.

Lemma sat_p_sat_compose : forall (rcld' : rcld) (dcl' : dcl) (ms' : ms) (p p' : P),  
  sat_comp_constr_p (introduced_method_constr ms' dcl' :: nil)  p = true -> compose_refines_class p rcld' = Some p' ->
  sat_comp_constr_p (introduced_method_constr ms' dcl' :: nil) p' = true.
  induction p; simpl.
  intros; discriminate.
  destruct a; destruct rcld'; case (eq_nat_dec d0 dcl'); caseEq (compose_refined_mds l l1).
  unfold sat_meth_constr_p at 1; simpl; case (eq_nat_dec d d0); simpl; intros; subst.
  generalize H0; clear H0; inversion H1; unfold sat_meth_constr_p; simpl; 
    case (eq_nat_dec dcl' dcl'); simpl; intros.
  destruct (andb_prop _ _ H0); apply andb_true_intro; pa.
  import (in_mds_in_compose _ _ _ _ H3 H).
  apply in_mds_in_introduce; auto.
  congruence.
  generalize H0; clear H0; unfold sat_meth_constr_p; simpl; 
    case (eq_nat_dec dcl' d); simpl.
  congruence.
  fold (sat_meth_constr_p dcl' ms' p); fold (sat_meth_constr_p dcl' ms' p'); intros.
  intros; destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; inversion H1.
  simpl in IHp.
  import (IHp _ H0 H2).
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec dcl' d).
  congruence.
  fold (sat_meth_constr_p dcl' ms' x).
  auto.
  case (eq_nat_dec d d0).
  intros; discriminate.
  unfold sat_meth_constr_p at 1; simpl; case (eq_nat_dec dcl' d).
  congruence.
  fold (sat_meth_constr_p dcl' ms' p); intros.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; inversion H1.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec dcl' d).
  congruence.
  fold (sat_meth_constr_p dcl' ms' x).
  intros; apply (IHp _ H0 H2).
  case (eq_nat_dec d d0).
  unfold sat_meth_constr_p at 1; simpl; case (eq_nat_dec dcl' d).
  congruence.
  fold (sat_meth_constr_p dcl' ms' p); intros.  
  inversion H1; subst; clear H1.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec dcl' d0).  
  congruence.
  fold (sat_meth_constr_p dcl' ms' p); auto.
  unfold sat_meth_constr_p at 1; simpl; case (eq_nat_dec dcl' d); simpl; intros.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; inversion H1.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec dcl' d); simpl.
  intros; destruct (andb_prop _ _ H0); apply andb_true_intro; pa.
  fold (sat_meth_constr_p dcl' ms' x).
  intros; destruct (andb_prop _ _ H0); apply andb_true_intro; pa.
  congruence.
  fold (sat_meth_constr_p dcl' ms' p) in H0.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; inversion H1.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec dcl' d); intros.
  congruence.
  fold (sat_meth_constr_p dcl' ms' x).  
  simpl in IHp; auto.
  case (eq_nat_dec d d0).
  intros; discriminate.
  unfold sat_meth_constr_p at 1; simpl; case (eq_nat_dec dcl' d); simpl; intros.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; inversion H1.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec dcl' d); simpl.
  intros; destruct (andb_prop _ _ H0); apply andb_true_intro; pa.
  fold (sat_meth_constr_p dcl' ms' x).
  intros; destruct (andb_prop _ _ H0); apply andb_true_intro; pa.
  congruence.
  fold (sat_meth_constr_p dcl' ms' p) in H0.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; inversion H1.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec dcl' d); intros.
  congruence.
  fold (sat_meth_constr_p dcl' ms' x).  
  simpl in IHp; auto.
Qed.

Lemma sat_rmds_sat_compose : forall (rcld' : rcld) (dcl' : dcl) (rmds : list rmd) (p p' : P),  
  sat_comp_constr_p (gen_meth_comp_constr rmds dcl') p = true -> compose_refines_class p rcld' = Some p' ->
  sat_comp_constr_p (gen_meth_comp_constr rmds dcl') p' = true.
  induction rmds.
  simpl; auto.
  destruct a; simpl.
  intros.
  destruct (andb_prop _ _ H).
  rewrite (IHrmds _ _ H2 H0).
  apply (sat_p_sat_compose rcld' dcl' m p p'); auto.
  simpl; rewrite H1; simpl; auto.
Qed.

Lemma distinct_introduced_names : forall (cld_list1 cld_list2: list cld), 
  distinct _ (names cld_list1) -> distinct _ (names (introduce_classes cld_list1 cld_list2)).
  induction cld_list2.
  simpl; auto.
  simpl.
  intros H; import (IHcld_list2 H); clear H IHcld_list2.
  destruct a.
  induction (introduce_classes cld_list1 cld_list2).
  simpl; pa.
  unfold not; intros H; bd H.
  discriminate.
  destruct a; simpl in H0; bd H0; import (IHl0 H0).
  simpl; case (eq_nat_dec d d0); intros.
  simpl in H.
  exact H.
  simpl; pa.
  unfold not; intros.
  bd H1. 
  congruence.
  simpl in H; bd H; auto.
  pa.
  unfold not; intro H1; apply H2; generalize n H1; clear; induction l0.
  simpl; auto.
  simpl; destruct a; case (eq_nat_dec d d1); intros.
  simpl; po2.
  auto.
  simpl in *|-*.
  bd H1.
  po1.
  po2; auto.
  simpl in H; bd H.
Qed.  

Lemma In_rm_dcl_split : forall (cld1 cld2 : cld) (cld_list : list cld) , 
  In cld1 (rm_dcl cld_list cld2) <-> (names (cld1 :: nil) <> names (cld2 :: nil) /\ In cld1 cld_list).
  induction cld_list; repeat pa; intros.
  simpl in H; contradiction.
  destruct cld1; destruct cld2; simpl in H; bd H; congruence.
  destruct a; destruct cld2; simpl in H; bd H.
  generalize H; clear H; case (eq_nat_dec d0 d); intros.
  tauto.
  simpl in H; bd H.
  destruct cld1; simpl; congruence.
  tauto.
  destruct a; destruct cld2; simpl in H; bd H.
  generalize H; clear H; case (eq_nat_dec d0 d); intros.
  simpl; po2.
  tauto.
  simpl; simpl in H; bd H.
  po1.
  po2; tauto.
  destruct cld1; destruct cld2; destruct a; simpl in H; bd H.
  simpl; case (eq_nat_dec d0 d1); intros.
  congruence.
  simpl; po1.
  simpl.
  simpl; case (eq_nat_dec d0 d1); intros.
  applyI IHcld_list; pa.
  simpl; po2.
  applyI IHcld_list; pa.
Qed.

Lemma In_introduce_classes : forall (cld_list1 cld_list2 : list cld) (cld' : cld),
  In cld' (introduce_classes cld_list1 cld_list2) -> In cld' cld_list1 \/ In cld' (introduce_classes nil cld_list2).
  induction cld_list2; simpl; intros.
  simpl; po1.
  bd H.
  po2; po1.
  cs (names (cld' :: nil) = names (a :: nil)).  
  destruct cld'; destruct a; simpl in H0; inversion H0; subst; clear H0.
  elimtype False; generalize H; clear; induction (introduce_classes cld_list1 cld_list2).
  simpl; auto.
  simpl; destruct a; case (eq_nat_dec d0 d); intros.
  auto.
  simpl in H; bd H; auto.
  congruence.
  assert (In cld' (introduce_classes cld_list1 cld_list2)).
  destruct cld'; destruct a; simpl in H0.
  assert (d <> d0).
  congruence.
  clear H0.
  generalize H H1; clear; induction (introduce_classes cld_list1 cld_list2).
  simpl; intros; exact H.
  destruct a; simpl; case (eq_nat_dec d0 d1); simpl; intros.
  po2; auto.
  bd H.
  po1.
  po2; auto.
  import (IHcld_list2 _ H1).
  bd H2.
  po1.
  repeat po2.
  destruct cld'; destruct a.
  assert (d <> d0).
  simpl in H0; congruence.
  generalize H2 H3; clear.
  induction (introduce_classes nil cld_list2).
  simpl; auto.
  simpl; destruct a; case (eq_nat_dec d0 d1); intros.
  bd H2.
  congruence.
  auto.
  simpl; bd H2.
  po1.
  po2; auto.
Qed.

Lemma In_rm_dcl : forall (cld' cld'': cld) (cld_list : list cld),
  In cld' (rm_dcl cld_list cld'') -> In cld' cld_list.
  induction cld_list.
  simpl; intros; contradiction.
  destruct a; destruct cld''; simpl; case (eq_nat_dec d0 d); intros.
  po2; auto.
  simpl in H; bd H.
  po1.
  po2; auto.  
Qed.

Lemma In_introduce_classes' : forall (cld_list1 cld_list2 : list cld) (cld' : cld),
  In cld' (introduce_classes nil cld_list2) -> In cld' (introduce_classes cld_list1 cld_list2).
  induction cld_list2; simpl; intros; bd H.
  po1.
  po2.
  import (IHcld_list2 _ (In_rm_dcl _ _ _ H)); clear IHcld_list2.
  cs (names (cld' :: nil) = names (a :: nil)).  
  destruct cld'; destruct a; simpl in H1; inversion H1; subst; clear H0.
  elimtype False; generalize H; clear; induction (introduce_classes nil cld_list2).
  simpl; auto.
  simpl; destruct a; case (eq_nat_dec d0 d); intros.
  auto.
  simpl in H; bd H; auto.
  congruence.
  clear H.
  induction (introduce_classes cld_list1 cld_list2).
  simpl in H0; contradiction.
  simpl in H0; bd H0.
  subst.
  simpl in *|-*; destruct cld'; destruct a; simpl.
  case (eq_nat_dec d0 d); intros; subst.
  congruence.
  simpl; po1.
  simpl in *|-*; destruct a0; destruct a; simpl.
  case (eq_nat_dec d0 d); intros; subst; auto.
  simpl; po2; auto.
Qed.

Lemma not_In_introduce_classes : forall (cld_list1 cld_list2 : list cld) (cld' : cld),
  In cld' (introduce_classes cld_list1 cld_list2) -> ~ In cld' (introduce_classes nil cld_list2) -> In cld' cld_list1.
  induction cld_list2; simpl; intros.
  exact H.
  bd H0.
  bd H.
  apply IHcld_list2.
  apply (In_rm_dcl _ _ _ H).
  unfold not; intros H3; apply H2.
  destruct a; destruct cld'.
  assert (d <> d0).
  import ((proj1 (In_rm_dcl_split _ _ _)) H); bd H1; simpl in H6.
  congruence.
  generalize H3 H1; clear; induction (introduce_classes nil cld_list2).
  simpl; contradiction.
  simpl; destruct a; case (eq_nat_dec d d1); intros.
  bd H3.
  congruence.
  auto.
  simpl; bd H3; auto.
Qed.

Lemma not_In_introduce_classes' : forall (cld_list1 cld_list2 : list cld) (dcl' : dcl) (cl' : cl) (fds' : list fd) (mds' : list md),
  In (cld_def dcl' cl' fds' mds') (introduce_classes cld_list1 cld_list2) -> ~ In (cl_dcl dcl') (names (introduce_classes nil cld_list2)) ->
  In (cld_def dcl' cl' fds' mds') cld_list1.
  induction cld_list2; simpl; intros.
  exact H.
  destruct a; bd H0.
  bd H.
  apply IHcld_list2.
  simpl in H0; bd H0.
  congruence.
  simpl in H0; bd H0.
  congruence.
  simpl in H0; bd H0.
  import (In_rm_dcl _ _ _ H).
  apply IHcld_list2; auto.
  unfold not; intros; apply H2.
  generalize H0 H3; clear; induction (introduce_classes nil cld_list2).
  simpl; intros; congruence.
  simpl; destruct a; case (eq_nat_dec d d0); simpl; intros.
  bd H3.
  congruence.
  auto.
  bd H3.
  po1.
  po2; auto.
Qed.

Lemma In_head_introduce_classes : forall (cld_list1 cld_list2 : list cld) (cld1 cld2 : cld),
  In cld1 (introduce_classes (cld2 :: cld_list1) cld_list2) -> 
  In cld1 (introduce_classes (cld2 :: nil) cld_list2) \/ In cld1 (introduce_classes cld_list1 cld_list2).
  intros.
  cs (In cld1 (introduce_classes nil cld_list2)).
  clear H.
  po2.
  induction cld_list2.
  simpl in H0; contradiction.
  simpl in H0; bd H0; subst.
  simpl; po1.
  simpl in H0; destruct ((proj1 (In_rm_dcl_split _ _ _ )) H0).
  destruct cld1; destruct a; simpl in H.
  assert (d <> d0).
  congruence.
  po2.
  generalize d d0 c0 f0 l0 H0 H2; clear.
  induction cld_list2.
  simpl; contradiction.
  intros d d0; simpl; destruct a; case (eq_nat_dec d0 d1); simpl.
  intros; auto; rewrite e in H2.
  import (In_rm_dcl _ _ _ H0).
  import (IHcld_list2 _ _ _ _ _ H H2); subst.
  generalize H1; clear; induction (introduce_classes cld_list1 cld_list2).
  simpl; auto.
  simpl; destruct a; case (eq_nat_dec d1 d0); simpl; intros.
  auto.
  case (eq_nat_dec d1 d0); intros; try congruence.
  simpl; bd H1.
  po1.
  po2; auto.
  intros.
  bd H0.
  po1.
  po2.
  assert (d <> d1).
  import ((proj1 (In_rm_dcl_split _ _ _)) H0); bd H.
  import ((proj1 (In_rm_dcl_split _ _ _)) H); bd H1.
  simpl in H6; congruence.
  import ((proj1 (In_rm_dcl_split _ _ _)) H0); bd H1.
  import (IHcld_list2 _ _ _ _ _ H1 H).
  applyI In_rm_dcl_split.
  pa.
  destruct cld1.
  (*** One Split ***)
  cs (In (cl_dcl d) (names (introduce_classes nil cld_list2))).
  import (not_In_introduce_classes _ _ _ H H0).
  simpl in H2; bd H2; subst.
  (*** Another Split***)
  induction cld_list2.
  simpl in H1; bd H1; discriminate.
  destruct a; simpl in *.
  bd H0; bd H; bd H1.
  elimtype False; inversion H1; subst.
  generalize H; clear; induction (introduce_classes (cld_def d c f l :: cld_list1) cld_list2).
  simpl; auto.
  simpl; destruct a; case (eq_nat_dec d d0); intros.
  auto.
  simpl in H; bd H; congruence.
  cs (d = d0); subst.
  elimtype False; generalize H1; clear.
  induction (introduce_classes nil cld_list2).
  simpl; intros H; bd H; discriminate.
  destruct a; simpl; case (eq_nat_dec d0 d); simpl; intros; auto.
  bd H1; congruence.
  cs (In (cld_def d c f l) (introduce_classes nil cld_list2)).
  po1; po2; generalize H2 H4; clear.
  induction cld_list2.
  simpl; contradiction.
  destruct a; simpl; case (eq_nat_dec d0 d1); intros.
  bd H4.
  inversion H4; subst.
  applyI In_rm_dcl_split.
  applyI In_rm_dcl_split.
  simpl; pa.
  congruence.
  subst.
  applyI In_rm_dcl_split; simpl; pa.
  congruence.
  import ((proj1 (In_rm_dcl_split _ _ _)) H4); bd H.
  import (IHcld_list2 H2 H).
  import ((proj1 (In_rm_dcl_split _ _ _)) H0); bd H1.
  bd H4.
  simpl; po1.
  import ((proj1 (In_rm_dcl_split _ _ _)) H4); bd H.
  import (IHcld_list2 H2 H).
  simpl; po2.
  applyI In_rm_dcl_split; simpl; pa.
  congruence.
  applyI In_rm_dcl_split; simpl; pa.
  import ((proj1 (In_rm_dcl_split _ _ _)) H0); bd H1.
  import ((proj1 (In_rm_dcl_split _ _ _)) H); bd H5.
  assert (In (cl_dcl d) (names (introduce_classes nil cld_list2))).
  generalize H1; clear;  induction (introduce_classes nil cld_list2).
  simpl; auto.
  simpl; destruct a; case (eq_nat_dec d0 d1); intros.
  simpl; po2; auto.
  simpl in *|-*; bd H1; auto.
  destruct (IHcld_list2 H4 H6 H5).
  po1; po2.
  applyI In_rm_dcl_split; pa.
  repeat po2; applyI In_rm_dcl_split; pa.
  induction cld_list2.
  simpl in H1; bd H1; discriminate.
  destruct a; simpl in *.
  bd H0; bd H; bd H1.
  elimtype False; inversion H1; subst.
  generalize H; clear; induction (introduce_classes (cld2 :: cld_list1) cld_list2).
  simpl; auto.
  simpl; destruct a; case (eq_nat_dec d d0); intros.
  auto.
  simpl in H; bd H; congruence.
  cs (d = d0); subst.
  elimtype False; generalize H1; clear.
  induction (introduce_classes nil cld_list2).
  simpl; intros H; bd H; discriminate.
  destruct a; simpl; case (eq_nat_dec d0 d); simpl; intros; auto.
  bd H1; congruence.
  cs (In (cld_def d c f l) (introduce_classes nil cld_list2)).
  po2; po2; generalize H3 H2 H5; clear.
  induction cld_list2.
  simpl; contradiction.
  destruct a; simpl; case (eq_nat_dec d0 d1); intros.
  bd H5.
  inversion H5; congruence.
  applyI In_rm_dcl_split; simpl; pa.
  congruence.
  auto.
  applyI In_rm_dcl_split; simpl; pa.
  congruence.
  import ((proj1 (In_rm_dcl_split _ _ _)) H5); bd H.
  import (IHcld_list2 H3 H2 H).
  import ((proj1 (In_rm_dcl_split _ _ _)) H0); bd H1.
  bd H5.
  po1.
  import ((proj1 (In_rm_dcl_split _ _ _)) H5); bd H.
  import (IHcld_list2 H3 H2 H).
  simpl; po2.
  import ((proj1 (In_rm_dcl_split _ _ _)) H0); bd H1.
  applyI In_rm_dcl_split; pa.
  applyI In_rm_dcl_split; pa.
  import ((proj1 (In_rm_dcl_split _ _ _)) H); bd H6.  
  assert (In (cl_dcl d) (names (introduce_classes nil cld_list2))).
  generalize H3 H1; clear; induction (introduce_classes nil cld_list2).
  simpl; auto.
  destruct a; simpl; case (eq_nat_dec d0 d1); simpl; intros.
  po2; auto.
  bd H1.
  po1.
  po2; auto.
  destruct (IHcld_list2 H6 H5 H7).
  po1; po2; applyI In_rm_dcl_split; pa.
  repeat po2;  applyI In_rm_dcl_split; pa.
  import (not_In_introduce_classes' _ _ _ _ _ _ H H1).
  simpl in H2; bd H2; subst.
  po1.
  generalize H1; clear; induction cld_list2.
  simpl; intros; po1.
  destruct a; simpl; case (eq_nat_dec d d0); intros.
  bd H1.
  congruence.
  bd H1.
  po2; applyI In_rm_dcl_split; pa.
  simpl; congruence.
  apply IHcld_list2.
  unfold not; intros H; apply H0; generalize n H; clear; induction (introduce_classes nil cld_list2).
  simpl; auto.
  destruct a; simpl; case (eq_nat_dec d0 d1); intros.
  bd H.
  congruence.
  auto.
  bd H.
  simpl; po1.
  simpl; po2; auto.
  po2.
  generalize H1 H2; clear; induction cld_list2.
  simpl; intros; auto.
  destruct a; simpl; case (eq_nat_dec d d0); intros.
  bd H1.
  congruence.
  bd H1.
  po2; applyI In_rm_dcl_split; pa.
  simpl; congruence.
  apply IHcld_list2.
  unfold not; intros H; apply H0; generalize n H; clear; induction (introduce_classes nil cld_list2).
  simpl; auto.
  destruct a; simpl; case (eq_nat_dec d0 d1); intros.
  bd H.
  congruence.
  auto.
  bd H.
  simpl; po1.
  simpl; po2; auto.
  exact H2.
Qed.  

Lemma distinct_refines_class : forall (rcld' : rcld) (cld_list cld_list': list cld), 
  distinct _ (names cld_list) -> compose_refines_class cld_list rcld' = Some cld_list' -> 
  distinct _ (names cld_list').
  induction cld_list.
  simpl; intros; discriminate.
  destruct rcld'; destruct a; simpl; case (eq_nat_dec d0 d); intros.
  caseEq (compose_refined_mds l1 l0); intros; rewrite H1 in H0.
  inversion H0.
  simpl; bd H; pa.
  discriminate.
  bd H; destruct (cons_option_Some _ _ _ _ H0).
  import (IHcld_list _ H H1).
  rewrite H1 in H0; simpl in H0.
  inversion H0.
  simpl; pa.
  generalize x n H3 H1; clear; induction cld_list.
  simpl; intros; discriminate.
  simpl; destruct a; case (eq_nat_dec d1 d); case ( compose_refined_mds l1 l0 ); intros.
  inversion H1.
  simpl; unfold not; intros H; bd H.
  discriminate.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H in H1; simpl in H1; inversion H1.
  simpl; apply and_not_or; pa.
  simpl in H3; bd H3.
  simpl in H3; bd H3; apply (IHcld_list); auto.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H in H1; simpl in H1; inversion H1.
  simpl; apply and_not_or; pa; simpl in H3; bd H3.
  apply (IHcld_list); auto.
Qed.
  
Lemma distinct_compose_names : forall (ps : PS) (p : P), 
  compose_all ps = Some p -> distinct _ (names p).
  induction ps; simpl; intros.
  inversion H; simpl; tauto.
  caseEq (compose_all ps); intros; rewrite H0 in H.
  import (IHps _ H0); clear IHps H0.
  destruct a.
  generalize l l0 p p0 H H1; clear; simpl.
  induction l; simpl.
  induction l0; simpl; intros.
  congruence.
  inversion H; subst; clear H.
  generalize (IHl0 _ _ (refl_equal _) H1); clear; induction (introduce_classes p0 l0); intros.
  destruct a; simpl; pa.
  unfold not; intros.
  bd H0; congruence.
  destruct a0; simpl in H; bd H.
  destruct a; simpl; case (eq_nat_dec d0 d); intros.
  subst; simpl; pa.
  clear; induction l. 
  simpl; unfold not; intros H; bd H.
  discriminate.
  destruct a; simpl; case (eq_nat_dec d d0); unfold not; intros.
  auto.
  simpl in H; bd H; auto.
  congruence.
  simpl in IHl; destruct (IHl H); auto.
  pa.
  simpl; unfold not; intros.
  bd H0.
  congruence.
  simpl in IHl; destruct (IHl H); auto.
  simpl; pa.
  simpl in IHl; destruct (IHl H); auto.
  generalize n H2; clear; induction l.
  simpl; auto.
  destruct a; simpl; case (eq_nat_dec d0 d1); unfold not; intros.
  cs (d0 = d).
  auto.
  cs (In (cl_dcl d) (names l)).
  auto.
  apply IHl; auto.
  simpl in H; bd H.
  auto.
  cs (d0 = d).
  auto.
  cs (In (cl_dcl d) (names l)).
  auto.
  apply IHl; auto.
  import (IHl H).
  simpl in H0; bd H0.
  intros; caseEq (fold_right
            (fun (rcld' : rcld) (op : option P) =>
             match op with
             | Some p' => compose_refines_class p' rcld'
             | None => None (A:=P)
             end) (Some p0) l); intros; rewrite H0 in H.
  caseEq (compose_refines_class p1 a); intros; rewrite H2 in H.
  inversion H.
  import (IHl l0 (introduce_classes p1 l0) p0); clear IHl; rewrite H0 in H3.
  import (H3 (refl_equal _) H1).
  assert (distinct _ (names p1)).
  generalize p0 p1 H1 H0; clear.
  induction l; simpl.
  congruence.
  intros.
  caseEq (fold_right
           (fun (rcld' : rcld) (op : option P) =>
            match op with
            | Some p' => compose_refines_class p' rcld'
            | None => None (A:=P)
            end) (Some p0) l); intros; rewrite H in H0.
  import (IHl _ _ H1 H).
  apply (distinct_refines_class _ _ _ H2 H0).
  discriminate.
  import (distinct_refines_class _ _ _ H6 H2).
  apply (distinct_introduced_names _ l0 H7).
  discriminate.
  discriminate.
  discriminate.
Qed.

Lemma sat_rmd_valid_compoe :  forall (dcl' : dcl) (cl' : cl) (rmds : list rmd) (mds : list md) (fds' : list fd) (p : P),
  sat_comp_constr_p (gen_meth_comp_constr rmds dcl') (cld_def dcl' cl' fds' mds :: p) = true ->
  exists mds', compose_refined_mds mds rmds = Some mds'.
  induction rmds; simpl; intros.
  exists mds; reflexivity.
  destruct a.
  simpl in H; destruct (andb_prop _ _ H).
  destruct (IHrmds _ _ _ H1); rewrite H2; clear H H1 IHrmds.
  unfold sat_meth_constr_p in H0.
  caseEq (path (cld_def dcl' cl' fds' mds :: p) (cl_dcl dcl')); intros; rewrite H in H0;
    simpl in H0.
  discriminate.
  destruct c.
  rewrite (path_eq_self _ _ _ _ _ _ _ H) in H.
  generalize H; clear H; simpl; case (eq_nat_dec d d); intros; inversion H; subst.
  assert (meth_in_mds x m = true).
  generalize l0 x m H0 H2; clear; induction rmds; simpl; intros.
  inversion H2; congruence.
  caseEq (compose_refined_mds l0 rmds); intros; rewrite H in H2.
  import (IHrmds _ _ _ H0 H).
  destruct a.
  destruct (in_mds_In_mds _ _ H1).
  destruct (In_mds_In_compose _ _ _ _ _ _ H2 H3).
  apply (In_mds_in_mds _ _ _ H4).
  discriminate.
  generalize m r H1; clear; induction x; intros.
  simpl in H1; discriminate.
  destruct a; simpl in H1.
  simpl;  destruct m1; destruct r.
  caseEq (ms_eq m0 m); intros.
  exists (md_def m0 (mb_def (s0 ++ s ++ s1) x1) :: x); reflexivity.
  caseEq (ms_eq m m0); intros; rewrite H0 in H1.
  rewrite ((proj1 (eq_ms_eq _ _ )) H0) in H.
  rewrite ((proj2 (eq_ms_eq _ _ )) (refl_equal m0)) in H; discriminate.
  unfold cons_option.
  destruct (IHx _ (rmb_def s0 s1 x1) H1).
  rewrite H2.
  exists (md_def m0 (mb_def s x0) :: x2); reflexivity.
  congruence.
Qed.

Lemma valid_compose_sat_rmd :  forall (dcl' : dcl) (cl' : cl) (rmds : list rmd) (mds mds' : list md) (fds' : list fd) (p : P),
  compose_refined_mds mds rmds = Some mds' ->
  sat_comp_constr_p (gen_meth_comp_constr rmds dcl') (cld_def dcl' cl' fds' mds :: p) = true.
  induction rmds; simpl; intros.
  reflexivity.
  destruct a.
  caseEq (compose_refined_mds mds rmds); intros; rewrite H0 in *.
  simpl.
  apply andb_true_intro; pa.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec dcl' dcl'); simpl; intros.
  generalize l mds' H0 H; clear; induction rmds; simpl; intros l mds'.
  intros; inversion H0; subst; clear H0.
  generalize mds' H; clear; induction l; intros mds' H; simpl in H.
  discriminate.
  destruct a; destruct m1; destruct r; caseEq (ms_eq m0 m); intros; rewrite H0 in *.
  clear IHl.
  rewrite ((proj1 (eq_ms_eq _ _ )) H0).
  simpl; rewrite ((proj2 (eq_ms_eq _ _ )) (refl_equal m)); reflexivity.
  destruct (cons_option_Some _ _ _ _ H); rewrite H1 in H; simpl in H.
  simpl; caseEq (ms_eq m m0); intros; auto; rewrite (IHl _ H1); auto.
  caseEq (compose_refined_mds mds rmds); intros.
  rewrite H in IHrmds.
  destruct a.
  assert (exists mds', compose_refined_md l0 (rmd_def m r) = Some mds').
  generalize mds' l H0 H1; clear; induction l0; intros mds'.
  simpl; intros; discriminate.
  simpl; destruct a; destruct m2; destruct r; destruct r0; 
    caseEq (ms_eq m1 m0); caseEq (ms_eq m1 m); intros.
  exists (md_def m1 (mb_def (s0 ++ s ++ s1) x0) :: l0); reflexivity.
  inversion H1; subst; simpl in H2; rewrite H in H2.
  destruct (cons_option_Some _ _ _ _ H2); rewrite H3; simpl.
  exists (md_def m1 (mb_def s x) :: x2); reflexivity.
  exists (md_def m1 (mb_def (s0 ++ s ++ s1) x0) :: l0); reflexivity.
  destruct (cons_option_Some _ _ _ _ H1); intros;
    rewrite H3 in IHl0; rewrite H3 in H1; simpl in H1; inversion H1.
  rewrite <- H5 in H2; simpl in H2; rewrite H in H2.
  destruct (cons_option_Some _ _ _ _ H2).
  destruct (IHl0 _ _ (refl_equal _) H4).
  rewrite H6; simpl; exists (md_def m1 (mb_def s x) :: x4); reflexivity.
  destruct H2.
  apply (IHrmds _ _ (refl_equal _) H2).
  discriminate.
  congruence.
  apply (IHrmds _ _ fds' p H0).
  discriminate.
Qed.

Lemma in_clds_compose' : forall (dcl' : dcl) (cl': cl) (rmds : list rmd) (mds : list md) (fds' : list fd) (p p': P),
  in_clds dcl' p = true ->  compose_refines_class p (refines_cld_def dcl' cl' fds' mds rmds) = Some p' ->
  in_clds dcl' p' = true.
  induction p.
  simpl; intros; discriminate.
  simpl; destruct a; case (eq_nat_dec d dcl'); caseEq (compose_refined_mds l rmds); intros.
  inversion H1; unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl; intros.
  reflexivity.
  congruence.
  discriminate.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; simpl in H1; inversion H1.
  generalize H0; clear H0; unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl.
  congruence.
  fold (in_clds dcl' p); fold (in_clds dcl' x); intros.
  apply IHp; auto.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H2 in H1; simpl in H1; inversion H1.
  generalize H0; clear H0; unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl.
  congruence.
  fold (in_clds dcl' p); fold (in_clds dcl' x); intros.
  apply IHp; auto.
Qed.

Lemma compose_in_clds : forall (dcl' : dcl) (cl': cl) (rmds : list rmd) (mds : list md) (fds' : list fd) (p p': P),
  compose_refines_class p (refines_cld_def dcl' cl' fds' mds rmds) = Some p' ->
  in_clds dcl' p = true.
  induction p.
  simpl; intros; discriminate.
  simpl; destruct a; case (eq_nat_dec d dcl'); caseEq (compose_refined_mds l rmds); intros.
  subst; unfold in_clds; simpl; case (eq_nat_dec dcl' dcl'); simpl; intros.
  reflexivity.
  congruence.
  discriminate.
  destruct (cons_option_Some _ _ _ _ H0); import (IHp _ H1).
  unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl; intros.
  congruence.
  auto.
  destruct (cons_option_Some _ _ _ _ H0); import (IHp _ H1).
  unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl; intros.
  congruence.
  auto.
Qed.

Lemma compose_in_clds' : forall (dcl' dcl'': dcl) (cl': cl) (rmds : list rmd) (mds : list md) (fds' : list fd) (p p': P),
  in_clds dcl' p' = true -> compose_refines_class p (refines_cld_def dcl'' cl' fds' mds rmds) = Some p' ->
  dcl' <> dcl'' -> in_clds dcl' p = true.
  induction p.
  simpl; intros; discriminate.
  simpl; destruct a; case (eq_nat_dec d dcl''); caseEq (compose_refined_mds l rmds); intros.
  generalize H0; clear H0; inversion H1; unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl; intros.
  congruence.
  exact H0.
  discriminate.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H3 in H1; simpl in H1; inversion H1; subst.
  generalize H0; clear H0; inversion H1; unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl; intros.
  reflexivity.
  fold (in_clds dcl' x) in H0; apply (IHp _ H0 H3).
  auto.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H3 in H1; simpl in H1; inversion H1; subst.
  generalize H0; clear H0; inversion H1; unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl; intros.
  reflexivity.
  fold (in_clds dcl' x) in H0; apply (IHp _ H0 H3).
  auto.
Qed.

Lemma in_clds_compose : forall (dcl' dcl'': dcl) (cl': cl) (rmds : list rmd) (mds : list md) (fds' : list fd) (p p': P),
  in_clds dcl' p = true ->  compose_refines_class p (refines_cld_def dcl'' cl' fds' mds rmds) = Some p' ->
  dcl' <> dcl'' -> in_clds dcl' p' = true.
  induction p.
  simpl; intros; discriminate.
  simpl; destruct a; case (eq_nat_dec d dcl''); caseEq (compose_refined_mds l rmds); intros.
  generalize H0; clear H0; inversion H1; unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl; intros.
  congruence.
  exact H0.
  discriminate.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H3 in H1; simpl in H1; inversion H1.
  generalize H0; clear H0; unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl.
  auto.
  fold (in_clds dcl' p); fold (in_clds dcl' x); intros.
  apply IHp; auto.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H3 in H1; simpl in H1; inversion H1.
  generalize H0; clear H0; unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl.
  congruence.
  fold (in_clds dcl' p); fold (in_clds dcl' x); intros.
  apply IHp; auto.
Qed.

Lemma sat_not_introduced : forall (dcl' : dcl) (p p' : P) (m : ms),
  in_path p' dcl' = false -> sat_meth_constr_p dcl' m p = true -> 
  sat_meth_constr_p dcl' m (introduce_classes p p') = true.
  induction p'; simpl.
  auto.
  destruct a; simpl; case (eq_nat_dec dcl' d).
  intros; discriminate.
  unfold sat_meth_constr_p at 2; simpl; case (eq_nat_dec dcl' d); simpl.
  congruence.
  intros _ n m.
  fold (sat_meth_constr_p dcl' m (rm_dcl (introduce_classes p p') (cld_def d c f l))).
  intros H H0; generalize n (IHp' _ H H0); clear.
  induction (introduce_classes p p'); simpl; auto.
  unfold sat_meth_constr_p; destruct a; case (eq_nat_dec d d0); simpl; 
    case (eq_nat_dec dcl' d0).
  congruence.
  intros; auto.
  simpl; auto.
  auto.
Qed.

Lemma sat_not_introduced' : forall (dcl' : dcl) (p p' : P) (m : ms),
  in_path p' dcl' = false  ->  sat_meth_constr_p dcl' m (introduce_classes p p') = true ->
  sat_meth_constr_p dcl' m p = true.
  induction p'; simpl; auto.
  destruct a; simpl; case (eq_nat_dec dcl' d).
  intros; discriminate.
  unfold sat_meth_constr_p at 1; simpl; case (eq_nat_dec dcl' d); simpl.
  congruence.
  intros _ n m.
  fold (sat_meth_constr_p dcl' m (rm_dcl (introduce_classes p p') (cld_def d c f l))).
  intros H H0; apply IHp'; auto.
  generalize H0 n; clear; induction (introduce_classes p p'); simpl; auto.
  unfold sat_meth_constr_p; destruct a; case (eq_nat_dec d d0); simpl; 
    case (eq_nat_dec dcl' d0).
  congruence.
  intros; auto.
  simpl; auto.
  auto.
Qed.  

Lemma sat_rcld_in_clds : forall (dcl' : dcl) (rmd' : rmd) (rmds : list rmd) (p : P),
  sat_comp_constr_p (gen_meth_comp_constr (rmd' :: rmds) dcl') p = true -> 
  in_clds dcl' p = true.
  destruct rmd'; simpl; intro rmds; induction (gen_meth_comp_constr rmds dcl'); simpl.
  intros p H; destruct (andb_prop _ _ H).
  generalize H0; clear; induction p.
  unfold sat_meth_constr_p; simpl; intros; discriminate.
  destruct a; unfold sat_meth_constr_p; unfold in_clds; simpl; case (eq_nat_dec dcl' d); auto.
  destruct a; simpl; intros p H; destruct (andb_prop _ _ H);
    destruct (andb_prop _ _ H1); import (IHl p); auto.
  apply H4; apply andb_true_intro; pa.
  apply H4; apply andb_true_intro; pa.
Qed.

Lemma sat_rcld_valid_compose : forall (dcl' : dcl) (cl': cl) (rmds : list rmd) (mds : list md) (fds' : list fd) (p : P),
  in_clds dcl' p = true -> sat_comp_constr_p (gen_meth_comp_constr rmds dcl') p = true -> 
  exists p', compose_refines_class p (refines_cld_def dcl' cl' fds' mds rmds) = Some p'.
  intros;  unfold in_clds in H.
  caseEq (path p(cl_dcl dcl')); intros; rewrite H1 in H; simpl in H.
  discriminate.
  destruct c; import (path_eq_self _ _ _ _ _ _ _ H1); subst.
  assert (In (cld_def d c f l0) (path p (cl_dcl d))). 
  subst; rewrite H1; simpl; po1.
  import (in_path_in_prog _ _ _ H2); clear H2 H1 H.
  induction p.
  simpl in H3; contradiction.
  destruct a.
  simpl.
  case (eq_nat_dec d0 d); intros.
  subst; destruct (sat_rmd_valid_compoe _ _ _ _ _ _ H0); rewrite H.
  exists (cld_def d cl' (introduce_fields f0 fds') (introduce_methods x mds) :: p); reflexivity.  
  simpl in H0.
  assert (sat_comp_constr_p (gen_meth_comp_constr rmds d) p = true).
  generalize n H0; clear.
  induction rmds; intros; simpl in H0.
  simpl; reflexivity.
  destruct a; simpl in *|-*.
  destruct (andb_prop _ _ H0).
  rewrite (IHrmds n H1).
  unfold sat_meth_constr_p in H.
  assert (path (cld_def d0 c0 f0 l1 :: p) (cl_dcl d) = path p (cl_dcl d)).
  simpl; case (eq_nat_dec d d0); congruence.
  rewrite H2 in H; fold (sat_meth_constr_p d m p) in H; rewrite H.
  reflexivity.
  simpl in H3; bd H3.
  congruence.
  destruct (IHp H H3).
  unfold cons_option; rewrite H1.
  exists (cld_def d0 c0 f0 l1 :: x); reflexivity.
Qed.

Lemma valid_compose_sat_p : forall (dcl' : dcl) (cl': cl) (rmds : list rmd) (mds : list md) (fds' : list fd) (p p' : P),
  compose_refines_class p (refines_cld_def dcl' cl' fds' mds rmds) = Some p' ->
  in_clds dcl' p = true /\ sat_comp_constr_p (gen_meth_comp_constr rmds dcl') p = true.
  intros; pa.
  generalize p' H; clear; induction p.
  simpl; intros; discriminate.
  destruct a; unfold in_clds; simpl; case (eq_nat_dec d dcl'); case (eq_nat_dec dcl' d);
    case (compose_refined_mds l rmds); simpl; intros; try congruence.
  fold (in_clds dcl' p); destruct (cons_option_Some _ _ _ _ H); rewrite H0 in H; simpl in H.
  apply (IHp _ H0).
  fold (in_clds dcl' p); destruct (cons_option_Some _ _ _ _ H); rewrite H0 in H; simpl in H.
  apply (IHp _ H0).
  generalize p' H; clear; induction p.
  simpl; intros; discriminate.
  destruct a; simpl; case (eq_nat_dec d dcl'); 
    caseEq (compose_refined_mds l rmds); simpl; intros; try congruence.
  subst; apply (valid_compose_sat_rmd dcl' c rmds l _ f p H).
  destruct (cons_option_Some _ _ _ _ H0).
  import (IHp _ H1).
  generalize n H2; clear; induction rmds.
  simpl; reflexivity.
  destruct a; simpl; intros.
  destruct (andb_prop _ _ H2); apply andb_true_intro; pa.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec dcl' d); simpl.
  congruence.
  fold (sat_meth_constr_p dcl' m p); auto.
  auto.
  destruct (cons_option_Some _ _ _ _ H0).
  import (IHp _ H1).
  generalize n H2; clear; induction rmds.
  simpl; reflexivity.
  destruct a; simpl; intros.
  destruct (andb_prop _ _ H2); apply andb_true_intro; pa.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec dcl' d); simpl.
  congruence.
  fold (sat_meth_constr_p dcl' m p); auto.
  auto.
Qed.

Lemma sat_rclds_fold' : forall (d : dcl) (l0 : list rmd) (rclds : list rcld) (p p0: P),
   fold_right (fun (rcld' : rcld) (op : option P) =>
      match op with
      | Some p'0 => compose_refines_class p'0 rcld'
      | None => None (A:=P)
      end) (Some p) rclds = Some p0 ->
   sat_comp_constr_rclds (gen_meth_comp_constr l0 d) rclds p = true ->
   sat_comp_constr_p (gen_meth_comp_constr l0 d) p0 = true.
  intros d l0; induction (gen_meth_comp_constr l0 d); simpl; intros rclds p.
  reflexivity.
  destruct a.
  intros p0 H H0 ; destruct (andb_prop _ _ H0); rewrite (IHl _ _ _ H H2);
    apply andb_true_intro; pa.
  generalize p0 H H1; clear; induction rclds.
  simpl; congruence.
  destruct a; simpl; case (eq_nat_dec d0 d).
  caseEq (meth_in_mds l m).
  caseEq ( fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p'0 => compose_refines_class p'0 rcld'
        | None => None (A:=P)
        end) (Some p) rclds); intros.
  subst.
  destruct (valid_compose_sat_p _ _ _ _ _ _ _ H1).
  generalize p1 H1 H0; clear; induction p0.
  simpl; intros; discriminate.
  destruct a; simpl; case (eq_nat_dec d0 d).
  caseEq (compose_refined_mds l1 l0); intros.
  inversion H1; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d d0); intros; simpl.
  apply (in_mds_in_introduce' m l2 l H0).
  congruence.
  discriminate.
  intros.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H in H1; simpl in H1; inversion H1.
  import (IHp0 _ H H0).
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec d d0); simpl.
  congruence.
  auto.
  discriminate.
  caseEq (fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p'0 => compose_refines_class p'0 rcld'
        | None => None (A:=P)
        end) (Some p) rclds); intros. 
  import (IHrclds _ H H2); import (compose_in_clds _ _ _ _ _ _ _ H1); subst;
    import (in_clds_compose' _ _ _ _ _ _ _ H4 H1).
  import (sat_p_sat_compose (refines_cld_def d c f l l0) d m p0 p1).
  simpl in H6; rewrite H3 in H6; simpl in H6; apply (proj1 (andb_prop _ _ (H6 (refl_equal _) H1))).
  discriminate.
  caseEq ( fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p'0 => compose_refines_class p'0 rcld'
        | None => None (A:=P)
        end) (Some p) rclds); intros; subst.
  import (IHrclds _ H H1).
  generalize p1 n H0 H2; clear; induction p0.
  simpl; intros; discriminate.
  destruct a; simpl; case (eq_nat_dec d1 d); subst.
  caseEq (compose_refined_mds l1 l0); intros.
  generalize H2; clear H2; subst; inversion H0; unfold sat_meth_constr_p; 
    simpl; case (eq_nat_dec d0 d); simpl; intros.
  import (in_mds_in_compose _ _ _ _ H1 H).
  apply (in_mds_in_introduce m l2 l H3).
  exact H1.
  discriminate.
  intros.
  destruct (cons_option_Some _ _ _ _ H0); rewrite H in H0; simpl in H0; inversion H0.
  cs (d1 = d0); subst.
  generalize H2; clear; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d0); simpl; auto.
  generalize H1 H2; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d1); simpl; auto.
  fold (sat_meth_constr_p d0 m p0); fold (sat_meth_constr_p d0 m x); intros.
  apply (IHp0 _ n0 H H4).
  discriminate.
  intros p0 H H0; destruct (andb_prop _ _ H0); rewrite (IHl _ _ _ H H2); apply andb_true_intro; pa.
  generalize p0 H H1; clear; induction rclds.
  simpl; congruence.
  destruct a; simpl; caseEq (fold_right (fun (rcld' : rcld) (op : option P) =>
      match op with
      | Some p'0 => compose_refines_class p'0 rcld'
      | None => None (A:=P)
      end) (Some p) rclds); intros. 
  import (IHrclds _ H H1).
  cs (d0 = d); subst.
  apply (in_clds_compose' _ _ _ _ _ _ _ H2 H0).
  apply (in_clds_compose _ _ _ _ _ _ _ _ H2 H0 H3).
  discriminate.
Qed.  

Lemma sat_comp_valid_compose : forall (clds : list cld) (rclds : list rcld) (c_list : list comp_constraint) (p : P),
  gen_cld_comp_constr rclds = c_list -> sat_comp_constr_p c_list p = true ->
  exists p', compose p (feature_def rclds clds) = Some p'.
  induction rclds.
  simpl; intros; exists (introduce_classes p clds); reflexivity.
  simpl; destruct a; intros.
  rewrite <- H in *.
  simpl in H0; destruct (andb_prop _ _ H0).
  destruct ((proj1 (sat_comp_constr_app_p _ _ _)) H2); 
    destruct (IHrclds _ _ (refl_equal _) H4); clear H H0 H2 IHrclds.
  unfold compose in H5.
  caseEq (fold_right
           (fun (rcld' : rcld) (op : option P) =>
            match op with
            | Some p' => compose_refines_class p' rcld'
            | None => None (A:=P)
            end) (Some p) rclds); intros; rewrite H in H5.
  assert (sat_comp_constr_p (gen_meth_comp_constr l0 d) p0 = true).
  generalize d c l0 p0 p H H1 H4 H3; clear; induction rclds; intros.
  simpl in H.
  inversion H; subst.
  exact H3.
  simpl in *; caseEq (fold_right
          (fun (rcld' : rcld) (op : option P) =>
           match op with
           | Some p' => compose_refines_class p' rcld'
           | None => None (A:=P)
           end) (Some p) rclds); intros.
  rewrite H0 in H.
  destruct a; simpl in H4; destruct (andb_prop _ _ H4).
  destruct ((proj1 (sat_comp_constr_app_p _ _ _) H5)).
  import (IHrclds _ c l0 _ _ H0 H1 H7 H3).
  apply (sat_rmds_sat_compose _ _ _ _ _ H8 H).
  rewrite H0 in H; discriminate.
  assert (in_clds d p0 = true).
  generalize p0 c H1 H; clear; induction rclds.
  simpl; intros; congruence.
  destruct a; simpl; caseEq (fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p' => compose_refines_class p' rcld'
        | None => None (A:=P)
        end) (Some p) rclds); intros.
  import (IHrclds _ c H1 H).
  cs (d0 = d); subst.
  apply (in_clds_compose' _ _ _ _ _ _ _ H2 H0).
  apply (in_clds_compose _ _ _ _ _ _ _ _ H2 H0).
  congruence.
  discriminate.
  destruct (sat_rcld_valid_compose _ c _ l f _ H2 H0); rewrite H6.
  exists (introduce_classes x0 clds); auto.
  discriminate.  
Qed.

Lemma safe_comp_valid_compose : forall (clds : list cld) (rclds : list rcld) (p : P),
  safe_compose_rclds rclds p = true ->
  exists p', compose p (feature_def rclds clds) = Some p'.
  induction rclds.
  simpl; intros; exists (introduce_classes p clds); reflexivity.
  simpl; destruct a; intros.
  simpl in H; destruct (andb_prop _ _ H); clear H.
  destruct (IHrclds _ H1); generalize H H0; clear.
  unfold compose.
  caseEq (fold_right
           (fun (rcld' : rcld) (op : option P) =>
            match op with
            | Some p' => compose_refines_class p' rcld'
            | None => None (A:=P)
            end) (Some p) rclds); intros.
  destruct (andb_prop _ _ H1).
  import (sat_rclds_fold' _ _ _ _ _ H H3).
assert (in_clds d p0 = true).
  generalize p0 H H2; clear; induction rclds.
  simpl; congruence.
  destruct a; simpl.
  caseEq (fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p' => compose_refines_class p' rcld'
        | None => None (A:=P)
        end) (Some p) rclds); intros.
  import (IHrclds _ H H2).
  cs (d = d0); subst.
  apply (in_clds_compose' _ c l0 l f p0 p1 H1 H0).
  apply (in_clds_compose _ _ c l0 l f p0 p1 H1 H0 H3).
  discriminate.
  destruct (sat_rcld_valid_compose _ c _ l f _ H5 H4).
  rewrite H6; exists (introduce_classes x0 clds); auto.
  discriminate.
Qed.  

Lemma sat_p_sat_rclds : forall (c_list : list comp_constraint) (rclds : list rcld) (p : P),
  sat_comp_constr_p c_list p = true -> sat_comp_constr_rclds c_list rclds p = true.
  induction c_list; simpl.
  auto.
  destruct a; simpl.
  intros rclds p H; destruct (andb_prop _ _ H); rewrite (IHc_list rclds _ H1); apply andb_true_intro; pa.
  generalize H0; clear; induction rclds.
  simpl; auto.
  intros H; destruct a; simpl; rewrite (IHrclds H); case (eq_nat_dec d d0); case (meth_in_mds l m); auto.
  intros rclds p H; destruct (andb_prop _ _ H); rewrite (IHc_list rclds p); auto.
  rewrite H0; reflexivity.
Qed.

Lemma sat_rclds_fold : forall (d : dcl) (l0 : list rmd) (rclds : list rcld) (p p0: P),
   fold_right (fun (rcld' : rcld) (op : option P) =>
      match op with
      | Some p'0 => compose_refines_class p'0 rcld'
      | None => None (A:=P)
      end) (Some p) rclds = Some p0 ->
   sat_comp_constr_rclds (gen_meth_comp_constr l0 d) rclds p0 = true ->
   sat_comp_constr_rclds (gen_meth_comp_constr l0 d) rclds p = true.
  intros d l0; induction (gen_meth_comp_constr l0 d); simpl; intros rclds p.
  reflexivity.
  destruct a.
  intros p0 H H0 ; destruct (andb_prop _ _ H0); rewrite (IHl _ _ _ H H2);
    apply andb_true_intro; pa.
  generalize p0 H H1; clear; induction rclds.
  simpl; congruence.
  destruct a; simpl; case (eq_nat_dec d0 d).
  caseEq (meth_in_mds l m).
  reflexivity.
  caseEq ( fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p'0 => compose_refines_class p'0 rcld'
        | None => None (A:=P)
        end) (Some p) rclds); intros.
  apply (IHrclds _ H); subst.
  generalize p1 H1 H2 H0; clear; induction p0.
  simpl; intros; discriminate.
  destruct a; simpl; case (eq_nat_dec d0 d).
  caseEq (compose_refined_mds l1 l0); intros; inversion H1; subst.
  clear H1 IHp0; generalize l2 l1 H H0 H2; clear.
  induction rclds.
  simpl; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d d); simpl; intros.
  import (in_introduce_in_mds _ _ _ H2 H0).
  exact (in_compose_in_mds _ _ _ _ H1 H).
  exact H2.
  destruct a; simpl; case (eq_nat_dec d d0).
  intros e l3 l4; caseEq (compose_refined_mds l4 l0); intros; inversion H1; subst.
  caseEq (meth_in_mds l1 m); intros; rewrite H3 in H2.
  reflexivity.
  apply (IHrclds _ _ H H1); auto; congruence.
  caseEq (meth_in_mds l1 m); intros; rewrite H3 in H2.
  reflexivity.
  discriminate.
  intros.
  apply (IHrclds _ _ H H0 H2).
  intros.
  destruct (cons_option_Some _ _ _ _ H1); rewrite H in H1; simpl in H1; inversion H1; subst.
  assert (forall x, sat_meth_constr_rclds' d m rclds (cld_def d0 c0 f0 l1 :: x) = sat_meth_constr_rclds' d m rclds x).
  generalize n; clear; induction rclds; simpl.
  unfold sat_meth_constr_p at 1; simpl; case (eq_nat_dec d d0); simpl.
  congruence.
  auto.
  intros; rewrite IHrclds; auto.
  rewrite H3 in *.
  apply (IHp0 _ H H2 H0).
  discriminate.
  caseEq (fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p'0 => compose_refines_class p'0 rcld'
        | None => None (A:=P)
        end) (Some p) rclds); intros.
  apply (IHrclds _ H).
  generalize n p1 H0 H1; clear; induction p0.
  simpl; intros; discriminate.
  destruct a; simpl; case (eq_nat_dec d1 d).
  destruct (compose_refined_mds l1 l0).
  intros; inversion H0; subst; generalize n H1; clear; induction rclds.
  simpl; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d); simpl.
  congruence.
  auto.
  destruct a; simpl; case (eq_nat_dec d0 d1).
  destruct (meth_in_mds l0 m); auto.
  intros; apply IHrclds; auto.
  intros; discriminate.
  intros.
  destruct (cons_option_Some _ _ _ _ H0); rewrite H in H0; simpl in H0; 
    inversion H0; rewrite <- H3 in *.
  cs (d1 = d0); subst.
  generalize H1; clear; induction rclds.
  simpl; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d0); simpl; auto.
  destruct a; simpl; case (eq_nat_dec d0 d).
  destruct (meth_in_mds l m); auto.
  intros; auto.
  assert (forall x, sat_meth_constr_rclds' d0 m rclds (cld_def d1 c0 f0 l1 :: x) = sat_meth_constr_rclds' d0 m rclds x).
  generalize n n0 H2; clear; induction rclds; simpl.
  unfold sat_meth_constr_p at 1; simpl; case (eq_nat_dec d0 d1); simpl.
  congruence.
  auto.
  intros; rewrite IHrclds; auto.
  rewrite H3 in *|-*.
  apply (IHp0 n0 _ H H1).
  discriminate.
  intros p0 H H0; destruct (andb_prop _ _ H0); rewrite (IHl _ _ _ H H2); apply andb_true_intro; pa.
  generalize p0 H H1; clear; induction rclds.
  simpl; congruence.
  destruct a; simpl; caseEq (fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p'0 => compose_refines_class p'0 rcld'
        | None => None (A:=P)
        end) (Some p) rclds); intros.
  cs (d0 = d); subst.
  apply (IHrclds _ H (compose_in_clds _ _ _ _ _ _ _ H0)).
  apply (IHrclds _ H (compose_in_clds' _ _ _ _ _ _ _ _ H1 H0 H2)).
  discriminate.
Qed.

Lemma valid_compose_sat_comp : forall (clds : list cld) (rclds : list rcld) (c_list : list comp_constraint) (p p': P),
  compose p (feature_def rclds clds) = Some p' -> safe_compose_rclds rclds p = true.
  induction rclds.
  simpl; intros; subst; simpl; reflexivity.
  destruct a; simpl.
  intros c_list p p'; caseEq (fold_right
         (fun (rcld' : rcld) (op : option P) =>
          match op with
          | Some p'0 => compose_refines_class p'0 rcld'
          | None => None (A:=P)
          end) (Some p) rclds).
  intro p0; caseEq (compose_refines_class p0 (refines_cld_def d c f l l0)).
  (*** intros; rewrite <- H2; simpl.***)
  intros; apply andb_true_intro; pa.
  destruct (valid_compose_sat_p _ _ _ _ _ _ _ H).
  import (sat_p_sat_rclds _ rclds _ H3).
  apply andb_true_intro; pa.
  generalize p0 H0 H2; clear; induction rclds.
  simpl; congruence.
  destruct a; simpl.
  caseEq (fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p'0 => compose_refines_class p'0 rcld'
        | None => None (A:=P)
        end) (Some p) rclds); intros.
  apply (IHrclds _ H ).
  cs (d = d0); subst.
  apply (compose_in_clds _ _ _ _ _ _ _ H0).
  apply (compose_in_clds' _ _ _ _ _ _ _ _ H2 H0 H1).
  discriminate.
  apply (sat_rclds_fold _ _ _ _ _ H0 H4).
  apply (IHrclds c_list p (introduce_classes p0 clds)).
  unfold compose; rewrite H0; reflexivity.
  intros; discriminate.
  intros; discriminate.
Qed.

Lemma sat_meth_rm_dcl : forall (dcl' dcl'' : dcl) (cl' : cl) (fds' : list fd) (mds' : list md) (ms' : ms) (p : P),
  dcl'' <> dcl' -> (sat_meth_constr_p dcl'' ms' (rm_dcl p (cld_def dcl' cl' fds' mds')) = true <->
    (sat_meth_constr_p dcl'' ms' p = true)).
  induction p; simpl.
  tauto.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec dcl' d); case (eq_nat_dec dcl'' d); simpl.
  congruence.
  intros _ _ n; pa; intros; applyI (IHp n); auto.
  case (eq_nat_dec dcl'' d); simpl; tauto.
  case (eq_nat_dec dcl'' d); simpl; tauto.
Qed.

Theorem sat_comp_ps_sat_p : forall (c_list : list comp_constraint) (ps : PS) (p : P),
  sat_comp_constr_ps c_list ps = true -> compose_all ps = Some p -> 
  sat_comp_constr_p c_list p = true.
  induction c_list.
  simpl; intros; reflexivity.
  destruct a; simpl; intros; destruct (andb_prop _ _ H);
    rewrite (IHc_list ps p); auto; apply andb_true_intro; pa;
      generalize p H1 H0; clear; induction ps; intros.
  (**** Break One****)
  simpl in H1; discriminate.
  destruct a.
  simpl in H1.
  caseEq (in_path l0 d); intros H; rewrite H in H1.
  simpl in H0.
  destruct (compose_all ps);
    try destruct (fold_right
      (fun (rcld' : rcld) (op : option P) =>
        match op with
          | Some p' => compose_refines_class p' rcld'
          | None => None (A:=P)
        end) (Some p0)); inversion H0.
  generalize p1 H1; clear; induction l0.
  unfold sat_meth_constr_clds; simpl; intros; discriminate.
  destruct a; unfold sat_meth_constr_clds; unfold sat_meth_constr_p; 
    simpl; case (eq_nat_dec d d0); simpl.
  auto.
  fold (sat_meth_constr_clds l0 d m).
  intros; fold (sat_meth_constr_p d m (rm_dcl (introduce_classes p1 l0) (cld_def d0 c f l))).
  generalize (IHl0 p1 H1) n; clear; induction (introduce_classes p1 l0).
  simpl; auto.
  destruct a; simpl; case (eq_nat_dec d0 d1); simpl.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec d d1); simpl.
  congruence.
  intros; apply IHl1; auto.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec d d1); simpl; auto.
  caseEq (sat_meth_constr_rclds l d m); intros; rewrite H2 in H1.
  generalize p H0 H H2; clear; induction l; intros.
  simpl in H; discriminate.
  destruct a; simpl in H2; generalize H2; clear H2; case (eq_nat_dec d d0); intros; subst.
  simpl in H0.
  caseEq (compose_all ps); intros; rewrite H1 in H0.
  caseEq (fold_right (fun (rcld' : rcld) (op : option P) =>
              match op with
              | Some p' => compose_refines_class p' rcld'
              | None => None (A:=P)
              end) (Some p0) l); intros; rewrite H3 in H0.
  caseEq (compose_refines_class p1 (refines_cld_def d0 c f l1 l2)); intros; rewrite H4 in H0.
  inversion H0; clear H0.
  caseEq (meth_in_mds l1 m); intros G1; rewrite G1 in H2.
  simpl in G1.
  destruct (in_mds_In_mds _ _ G1).
  import (in_rclds_mds_in_p _ _ _ _ _ _ _ _ _ H4 H0).
  bd H5.
  import (distinct_compose_names _ _ H1).
  assert (distinct _ (names p1)).
  generalize p1 H3 H7; clear; induction l; simpl; intros.
  congruence.
  caseEq (fold_right
           (fun (rcld' : rcld) (op : option P) =>
            match op with
            | Some p' => compose_refines_class p' rcld'
            | None => None (A:=P)
            end) (Some p0) l); intros; rewrite H in H3.
  apply (distinct_refines_class _ _ _  (IHl _ H H7) H3).
  discriminate.
  simpl in H3.
  generalize H H5 H9 (distinct_refines_class _ _ _ H8 H4); clear; induction l0.
  simpl; intros _ H H0 H1.
  induction p2; simpl in H0.
  contradiction.
  bd H0; subst.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d0); simpl.
  intros; apply (In_mds_in_mds _ _ _ H).
  congruence.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d); simpl.
  simpl in H1; bd H1; intros; subst.
  import (In_names _ _ _ _ _ H0); tauto.
  intros; fold (sat_meth_constr_p d0 m p2).
  simpl in H1; bd H1; auto.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d); intros.
  congruence.
  fold (sat_meth_constr_p d0 m (rm_dcl (introduce_classes p2 l0) (cld_def d c0 f l))); bd H1.
  generalize (IHl0 H H5 H9 H0) n; clear; induction (introduce_classes p2 l0); simpl.
  auto.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d d1); 
    case (eq_nat_dec d0 d1); simpl; intros.
  congruence.
  fold (sat_meth_constr_p d0 m l1) in H; fold (sat_meth_constr_p d0 m  (rm_dcl l1 (cld_def d c0 f l))); auto.
  case (eq_nat_dec d0 d1); simpl; intros; auto.
  case (eq_nat_dec d0 d1); simpl; intros; auto.
  unfold compose_all in IHl; fold (compose_all ps) in IHl; rewrite H1 in IHl; 
    unfold compose in IHl; rewrite H3 in IHl; import (IHl _ (refl_equal _) H H2).
  generalize p2 H H4 G1 H0; clear; induction l0.
  simpl; induction p1.
  simpl; intros; discriminate.
  destruct a; simpl; case (eq_nat_dec d d0).
  caseEq (compose_refined_mds l l2); intros.
  inversion H4; subst; clear H4; generalize H1; unfold sat_meth_constr_p; simpl;
    case (eq_nat_dec d0 d0); simpl; intros.
  apply in_mds_in_introduce.
  apply (in_mds_in_compose _ _ _ _ H2 H).
  auto.
  discriminate.
  intros n p2 H H0 H1 H2; destruct (cons_option_Some _ _ _ _ H0); rewrite H3 in H0;
    simpl in H0; inversion H0; subst.
  generalize H2; clear H2; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d); auto.
  intros; apply (IHp1 x); auto.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d); simpl; auto.
  fold (sat_meth_constr_p d0 m (rm_dcl (introduce_classes p1 l0) (cld_def d c0 f0 l))); intros;
    fold (sat_meth_constr_p d0 m (rm_dcl (introduce_classes p2 l0) (cld_def d c0 f0 l))).
  applyI (sat_meth_rm_dcl _ _ c0 f0 l m (introduce_classes p2 l0) n).
  apply (IHl0 _ H H4 G1).
  applyI (sat_meth_rm_dcl _ _ c0 f0 l m (introduce_classes p1 l0) n).
(**** Original Proof Scripts****)
  discriminate.
  discriminate.
  discriminate.
  simpl in H0, IHl; destruct (compose_all ps).
  destruct ( fold_right
    (fun (rcld' : rcld) (op : option P) =>
      match op with
        | Some p' => compose_refines_class p' rcld'
        | None => None (A:=P)
      end) (Some p0) l).
  import (IHl _ (refl_equal _) H H2).
  caseEq (compose_refines_class p1 (refines_cld_def d0 c f l1 l2)); intros; rewrite H3 in H0.
  inversion H0.
  apply (sat_not_introduced d p2 l0 m H).
  import (sat_not_introduced' _ _ _ _ H H1).
  import (sat_p_sat_compose (refines_cld_def d0 c f l1 l2) d m p1 p2).
  simpl in H6; rewrite H4 in H6; simpl in H6; bd (andb_prop _ _ (H6 (refl_equal _) H3)).
  discriminate.
  discriminate.
  discriminate.
  simpl in H0; destruct (compose_all ps).
  import (IHps _ H1 (refl_equal _)).
  caseEq (fold_right
           (fun (rcld' : rcld) (op : option P) =>
            match op with
            | Some p' => compose_refines_class p' rcld'
            | None => None (A:=P)
            end) (Some p0) l); intros; rewrite H4 in H0.
  inversion H0.
  apply (sat_not_introduced d p1 l0 m H).
  generalize p1 H3 H4; clear; induction l.
  simpl; congruence.
  destruct a; simpl; intros.
  caseEq (fold_right
           (fun (rcld' : rcld) (op : option P) =>
            match op with
            | Some p' => compose_refines_class p' rcld'
            | None => None (A:=P)
            end) (Some p0) l); intros; rewrite H in H4.
  import (IHl _ H3 H).
  import (sat_p_sat_compose (refines_cld_def d0 c f l0 l1) d m p p1).
  simpl in H1; rewrite H0 in H1; simpl in H1; bd (andb_prop _ _ (H1 (refl_equal _) H4)).
  discriminate.
  discriminate.
  discriminate.  
  simpl in H1; discriminate.
  destruct a; simpl in H1.
  caseEq (in_clds d l0); intros; rewrite H in H1; simpl in H0.
  destruct (compose_all ps).
  destruct (fold_right
    (fun (rcld' : rcld) (op : option P) =>
      match op with
        | Some p' => compose_refines_class p' rcld'
        | None => None (A:=P)
      end) (Some p0) l).
  generalize p H0 H; clear; induction l0.
  unfold in_clds; simpl; intros; discriminate.
  destruct a; simpl; unfold in_clds; simpl; case (eq_nat_dec d d0); simpl;
    intros e p H H0; inversion H.
  simpl; case (eq_nat_dec d d0); simpl; congruence.
  simpl; case (eq_nat_dec d d0); simpl; try congruence.
  fold (in_clds d (rm_dcl (introduce_classes p1 l0) (cld_def d0 c f l))).
  fold (in_clds d l0) in H0.
  import (IHl0 _ (refl_equal _) H0).
  generalize H1; clear; induction (introduce_classes p1 l0).
  simpl; auto.
  destruct a; unfold in_clds; simpl; case (eq_nat_dec d0 d1); case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  case (eq_nat_dec d d1); simpl; congruence.
  case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  discriminate.
  discriminate.
 import (distinct_compose_names ps).
 destruct (compose_all ps).
 import (H2 _ (refl_equal _)); clear H2.
 import (IHps _ H1 (refl_equal _)).
  generalize p H H2 H0; clear; induction l; simpl.
 induction l0.
 simpl; congruence.
 destruct a; unfold in_clds; simpl; case (eq_nat_dec d d0); simpl; intros.
 discriminate.
 fold (in_clds d p0) in H2; fold (in_clds d p); fold (in_clds d l0) in H.
 import (IHl0 _ H H2 (refl_equal _)).
 inversion H0.
 unfold in_clds; simpl; case (eq_nat_dec d d0); simpl.
 reflexivity.
 fold (in_clds d  (rm_dcl (introduce_classes p0 l0) (cld_def d0 c f l) )).
 generalize H1; clear; induction  (introduce_classes p0 l0).
 simpl; auto.
 destruct a; unfold in_clds; simpl; case (eq_nat_dec d0 d1); case (eq_nat_dec d d1); simpl.
 congruence.
 fold (in_clds d l1); fold (in_clds d (rm_dcl l1 (cld_def d0 c f l))); auto.
 case (eq_nat_dec d d1); intros; subst.
 simpl; auto.
 congruence.
 case (eq_nat_dec d d1); simpl.
 congruence.
 fold (in_clds d l1); fold (in_clds d (rm_dcl l1 (cld_def d0 c f l))); auto. 
 caseEq (       fold_right
         (fun (rcld' : rcld) (op : option P) =>
          match op with
          | Some p' => compose_refines_class p' rcld'
          | None => None (A:=P)
          end) (Some p0) l); intros.
 rewrite H in IHl; import (IHl _ H0 H2 (refl_equal _)).
 assert (in_clds d p = true).
 generalize H0 H3; clear; induction l0.
 unfold in_clds; simpl; auto.
 unfold in_clds; destruct a; simpl; case (eq_nat_dec d d0); simpl.
 intros; discriminate.
 fold (in_clds d p); fold (in_clds d l0); 
   fold (in_clds d (rm_dcl (introduce_classes p l0) (cld_def d0 c f l))); intros.
 apply IHl0; auto.
 generalize n H3; clear; induction (introduce_classes p l0).
 simpl; auto.
  destruct a; unfold in_clds; simpl; case (eq_nat_dec d0 d1); case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  case (eq_nat_dec d d1); simpl; congruence.
  case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  caseEq (compose_refines_class p a); intros; rewrite H5 in H1; inversion H1; clear H1.
  assert (in_clds d p2 = true).
  destruct a; cs (d = d0); subst.
  apply (in_clds_compose' _ _ _ _ _ _ _ H4 H5).
  apply (in_clds_compose _ _ _ _ _ _ _ _ H4 H5 H1).
  generalize H0 H1; clear; induction l0.
  simpl; auto.
  destruct a; unfold in_clds; simpl; case (eq_nat_dec d d0); simpl.
  intros; discriminate.
  fold (in_clds d l0); fold (in_clds d p2); fold (in_clds d (rm_dcl (introduce_classes p2 l0) (cld_def d0 c f l))).
  intros n H H0; generalize n (IHl0 H H0); clear; induction (introduce_classes p2 l0).
 simpl; auto.
  destruct a; unfold in_clds; simpl; case (eq_nat_dec d0 d1); case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  case (eq_nat_dec d d1); simpl; congruence.
  case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  discriminate.
  discriminate.
Qed.

Lemma in_clds_in_p : forall (dcl' : dcl) (p : P),
  in_clds dcl' p = true -> exists cl, exists fds, exists mds, In (cld_def dcl' cl fds mds) p.
  induction p.
  simpl; intros; discriminate.
  destruct a; unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl.
  intros; subst; exists c; exists f; exists l; po1.
  fold (in_clds dcl' p); intros n H; import (IHp H); bd H0.
  exists x; exists x0; exists x1; po2.
Qed.
  
Lemma in_p_in_clds : forall (dcl' : dcl) (cl' : cl) (fds' : list fd) (mds' : list md) (p : P),
  In (cld_def dcl' cl' fds' mds') p -> in_clds dcl' p = true.
  induction p; simpl.
  contradiction.
  intros H; bd H; subst.
  unfold in_clds; simpl; case (eq_nat_dec dcl' dcl'); simpl.
  reflexivity.
  congruence.
  destruct a; unfold in_clds; simpl; case (eq_nat_dec dcl' d); simpl.
  reflexivity.
  auto.
Qed.

Lemma in_clds_compose_ps : forall (dcl' : dcl) (ps : PS) (p : P),
  compose_all ps = Some p ->  in_clds dcl' p = true -> sat_cld_constr_ps dcl' ps = true.
  induction ps.
  simpl; intros; inversion H; subst; unfold in_clds in H0; simpl in H0; exact H0.
  destruct a; simpl; caseEq (compose_all ps).
  caseEq (in_clds dcl' l0); auto.
  intros H p; caseEq (fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p' => compose_refines_class p' rcld'
        | None => None (A:=P)
        end) (Some p) l); intros.
  inversion H2; rewrite <- H5 in H3.
  assert (in_clds dcl' p0 = true).
  import (in_clds_in_p _ _ H3); bd H4.
  apply (in_p_in_clds dcl' x x0 x1).
  apply (not_In_introduce_classes p0 l0 _ H4).
  generalize H; clear; induction l0; unfold in_clds; simpl.
  tauto.
  destruct a; case (eq_nat_dec dcl' d); simpl.
  intros; discriminate.
  fold (in_clds dcl' l0); intros.
  unfold not; intro H0; bd H0.
  congruence.
  apply (IHl0 H).
  generalize n H0; clear; induction (introduce_classes nil l0).
  simpl; auto.
  destruct a; simpl; case (eq_nat_dec d d0).
  intros; po2; auto.
  simpl; intros n n0 H0.
  bd H0.
  po1.
  po2; auto.
  apply (IHps p H1).
  generalize p0 H0 H4; clear; induction l.
  simpl; congruence.
  simpl.
  caseEq (fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p' => compose_refines_class p' rcld'
        | None => None (A:=P)
        end) (Some p) l); intros.
  apply (IHl _ H ).
  destruct a; cs (dcl' = d); subst.
  apply (compose_in_clds _ _ _ _ _ _ _ H0).
  apply (compose_in_clds' _ _ _ _ _ _ _ _ H4 H0 H1).
  discriminate.
  discriminate.
  intros; discriminate.
Qed.

Theorem sat_p_sat_comp_ps : forall (c_list : list comp_constraint) (ps : PS) (p : P),
   compose_all ps = Some p -> sat_comp_constr_p c_list p = true ->
   sat_comp_constr_ps c_list ps = true.
  induction c_list.
  simpl; intros; reflexivity.
  destruct a; simpl; intros ps p H0 H; destruct (andb_prop _ _ H);
    rewrite (IHc_list ps p); auto; apply andb_true_intro; pa.
  generalize p H1 H0; clear; induction ps; intros.
  simpl in H0; inversion H0; subst.
  unfold sat_meth_constr_p in H1; simpl in H1; discriminate.
  destruct a; simpl in H0; caseEq (compose_all ps); intros; rewrite H in H0.
  caseEq (fold_right
           (fun (rcld' : rcld) (op : option P) =>
            match op with
            | Some p' => compose_refines_class p' rcld'
            | None => None (A:=P)
            end) (Some p0) l); intros; rewrite H2 in H0.
  inversion H0; subst; clear H0.
  unfold sat_meth_constr_ps; caseEq (in_path l0 d); intros.
  unfold sat_meth_constr_p in H1.
  generalize H1 H0; clear; induction l0.
  simpl; intros; discriminate.
  unfold sat_meth_constr_clds; destruct a; simpl; case (eq_nat_dec d d0); simpl.
  auto.
  fold (sat_meth_constr_clds l0 d m); fold (sat_meth_constr_p d m (introduce_classes p1 l0)) in IHl0.
  fold (sat_meth_constr_p d m (rm_dcl (introduce_classes p1 l0) (cld_def d0 c f l) )).  
  intros; apply IHl0; auto.
  generalize n H1; clear; induction (introduce_classes p1 l0); simpl.
  auto.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d1); case (eq_nat_dec d d1).
  congruence.
  auto.
  simpl; case (eq_nat_dec d d1); simpl; auto.
  simpl; case (eq_nat_dec d d1); simpl; auto.
  caseEq (sat_meth_constr_rclds l d m); auto; fold (sat_meth_constr_ps  d m ps).
  intros; apply (IHps p0); auto.
  assert (sat_meth_constr_p d m p1 = true).
  generalize H1 H0; clear.
  induction l0.
  simpl; auto.
  destruct a; simpl; case (eq_nat_dec d d0).
  intros; discriminate.
  unfold sat_meth_constr_p at 1; simpl; case (eq_nat_dec d d0); simpl.
  auto.
  fold (sat_meth_constr_p d m  (rm_dcl (introduce_classes p1 l0) (cld_def d0 c f l))); intros; 
    apply IHl0; auto.
  generalize n H1; clear; induction (introduce_classes p1 l0).
  simpl; auto.
  unfold sat_meth_constr_p; destruct a; simpl; case (eq_nat_dec d d1); case (eq_nat_dec d0 d1).
  congruence.
  simpl; case (eq_nat_dec d d1); simpl; auto.
  auto.
  simpl; case (eq_nat_dec d d1); simpl; auto.
  generalize p1 H4 H2 H3; clear; induction l.
  simpl; congruence.
  destruct a; simpl.
  case (eq_nat_dec d d0); caseEq (fold_right
    (fun (rcld' : rcld) (op : option P) =>
      match op with
        | Some p' => compose_refines_class p' rcld'
        | None => None (A:=P)
      end) (Some p0) l); intros.
  caseEq (meth_in_mds l0 m); intros; rewrite H0 in H3.
  discriminate.
  assert (sat_meth_constr_p d m p = true).
  generalize p1 H4 H2 H0; clear; induction p.
  simpl; intros; discriminate.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d d1); 
    case (eq_nat_dec d1 d0); intros.
  caseEq (compose_refined_mds l l1); intros; rewrite H in H2; inversion H2; subst; clear H2.
  simpl in H4; generalize H4; clear H4; case (eq_nat_dec d0 d0); simpl; intros.
  import (in_introduce_in_mds _ _ _ H4 H0).
  apply (in_compose_in_mds _ _ _ _ H1 H).
  congruence.
  simpl.
  destruct (cons_option_Some _ _ _ _ H2); rewrite H in H2; simpl in H2; inversion H2; subst.
  simpl in H4; generalize H4; clear H4; case (eq_nat_dec d1 d1); simpl; intros; auto.
  caseEq (compose_refined_mds l l1); intros; rewrite H in H2; inversion H2; subst; clear H2.
  simpl in H4; generalize H4; clear H4; case (eq_nat_dec d d0); simpl; intros; auto.
  destruct (cons_option_Some _ _ _ _ H2); rewrite H in H2; simpl in H2; inversion H2; subst.
  simpl in H4; generalize H4; clear H4; case (eq_nat_dec d d1); simpl; intros; auto.
  apply (IHp x); auto.
  apply (IHl _ H1 H H3).
  discriminate.
  apply (IHl p); auto.
  generalize p1 n H4 H2; clear; induction p.
  simpl; intros; discriminate.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d d1); 
    case (eq_nat_dec d1 d0); intros.
  congruence.
  simpl.
  destruct (cons_option_Some _ _ _ _ H2); rewrite H in H2; simpl in H2; inversion H2; subst.
  simpl in H4; generalize H4; clear H4; case (eq_nat_dec d1 d1); simpl; intros; auto.
  caseEq (compose_refined_mds l l1); intros; rewrite H in H2; inversion H2; subst; clear H2.
  simpl in H4; generalize H4; clear H4; case (eq_nat_dec d d0); simpl; intros; auto.
  destruct (cons_option_Some _ _ _ _ H2); rewrite H in H2; simpl in H2; inversion H2; subst.
  simpl in H4; generalize H4; clear H4; case (eq_nat_dec d d1); simpl; intros; auto.
  apply (IHp x); auto.
  discriminate.
  discriminate.
  discriminate.
  (*** case 2 of a***)
  apply (in_clds_compose_ps _ _ _ H0 H1).
Qed.

Lemma compose_ps_in_clds : forall (dcl' : dcl) (ps : PS) (p : P),
  compose_all ps = Some p -> sat_cld_constr_ps dcl' ps = true ->  in_clds dcl' p = true.
  intros; import (sat_comp_ps_sat_p (introduced_class_constr dcl' :: nil) ps p).
  simpl in H1; rewrite H0 in H1; simpl in H1; apply (proj1 (andb_prop _ _ (H1 (refl_equal _) H))).
  Qed.

Lemma compose_safe_comp : forall (ps : PS) (rclds : list rcld) (p : P),
  compose_all ps = Some p -> safe_compose_rclds_ps rclds ps = true ->
  safe_compose_rclds rclds p = true.
  induction rclds; simpl.
  reflexivity.
  destruct a; simpl; intros.
  destruct (andb_prop _ _ H0); clear H0.
  rewrite (IHrclds _ H H2).
  destruct (andb_prop _ _ H1); clear H1; repeat (apply andb_true_intro; pa).
  apply (compose_ps_in_clds d ps p H H0).
  generalize H H3; clear; induction (gen_meth_comp_constr l0 d).
  simpl; reflexivity.
  destruct a; simpl; intros H4 H; destruct (andb_prop _ _ H); clear H; apply andb_true_intro; pa.
  generalize H4 H0; clear; induction rclds; simpl.
  import (sat_comp_ps_sat_p (introduced_method_constr m d0 :: nil) ps p).
  simpl in H; intros H0 H1; rewrite H1 in H; simpl in H; apply (proj1 (andb_prop _ _ (H (refl_equal _) H0))).
  destruct a; case (eq_nat_dec d0 d); auto.
  case (meth_in_mds l m); auto.
  auto.
  apply (compose_ps_in_clds _ _ _ H4 H0).
  auto.
Qed.

Theorem sat_comp_valid_compose_f : forall (ps : PS),
  safe_compose ps = true -> exists p, compose_all ps = Some p.
  induction ps; intros.
  simpl; exists (nil : list cld); reflexivity.
  destruct a; simpl in H; destruct (andb_prop _ _ H).
  destruct (IHps H1).
  import (compose_safe_comp _ _ _ H2 H0).
  simpl; rewrite H2.
  assert (exists p', fold_right
         (fun (rcld' : rcld) (op : option P) =>
          match op with
          | Some p' => compose_refines_class p' rcld'
          | None => None (A:=P)
          end) (Some x) l = Some p').
  generalize H2 H3 H0; clear; induction l.
  simpl; exists x; auto.
  destruct a; simpl; intros H2 H3 H; destruct (andb_prop _ _ H); clear H; destruct (andb_prop _ _ H0); clear H0.
  destruct (andb_prop _ _ H3); clear H3; destruct (andb_prop _ _ H0); clear H0.
  destruct (IHl H2 H5 H1).
  import (sat_rclds_fold' _ _ _ _ _ H0 H6); rewrite H0.
  apply (sat_rcld_valid_compose d c l1 l0 f x0).
  generalize x0 H3 H0; clear; induction l.
  simpl; congruence.
  destruct a; simpl; caseEq (fold_right
       (fun (rcld' : rcld) (op : option P) =>
        match op with
        | Some p' => compose_refines_class p' rcld'
        | None => None (A:=P)
        end) (Some x) l); intros.
  import (IHl _ H3 H).
  cs (d = d0); subst.
  apply (in_clds_compose' _ _ _ _ _ _ _ H1 H0).
  apply (in_clds_compose _ _ _ _ _ _ _ _ H1 H0 H2).
  discriminate.
  exact H7.
  destruct H4; rewrite H4.
  exists (introduce_classes x0 l0); auto.
Qed.

Theorem compose_f_sat_comp_valid : forall (ps : PS) (p : P),
  compose_all ps = Some p -> safe_compose ps = true.
  induction ps; intros.
  simpl; reflexivity.
  destruct a.
  simpl in H; caseEq (compose_all ps); intros; rewrite H0 in H.
  simpl; rewrite (IHps _ H0).
  apply andb_true_intro; pa.
  fold (compose p0 (feature_def l l0)) in H.
  import (valid_compose_sat_comp _ _ nil _ _ H).
  clear IHps H.
  induction l; simpl.
  reflexivity.
  destruct a.
  simpl in H1; destruct (andb_prop _ _ H1); clear H1.
  destruct (andb_prop _ _ H); clear H.
  rewrite (IHl H2); repeat (apply andb_true_intro; pa).
  apply (in_clds_compose_ps _ _ _ H0 H1).
  generalize H3 H0; clear; induction (gen_meth_comp_constr l2 d).
  simpl; auto.
  destruct a; simpl; intros H H1; destruct (andb_prop _ _ H); rewrite IHl0; auto;
    apply andb_true_intro; pa; generalize H0 H1; clear. 
  induction l.
  simpl.
  intros H0 H1; import (sat_p_sat_comp_ps (introduced_method_constr m d0 :: nil) ps p0 H1).
  simpl in H; rewrite H0 in H; simpl in H; apply (proj1 (andb_prop _ _ (H (refl_equal _)))).
  destruct a; simpl; case (eq_nat_dec d0 d).
  destruct (meth_in_mds l0 m); auto.
  auto.
  intros H H0; apply (in_clds_compose_ps _ _ _ H0 H).
  discriminate.
Qed.

Theorem compose_f_sat_comp_valid_iff : forall (ps : PS),
  (exists p, compose_all ps = Some p) <-> safe_compose ps = true.
  pa; intros.
  destruct H.
  apply (compose_f_sat_comp_valid _ _ H).
  apply (sat_comp_valid_compose_f _ H).
Qed.