Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Natmap.
Require Import FMaps.
Require Import EqNat.
Require Import lj_definitions.
Require Import lj_infrastructure.
Require Import lj_soundness.
Require Import lj_constraint_definitions.
Require Import lj_constraint_infrastructure.
Require Import FMapFacts.
Require Import Natmap.
Require Import Classical.
Require Import base2.
Require Import Max.

Lemma sat_fieldr_constr : forall (p : P) (ty' : ty) (dcl' : dcl) (f' : f), 
  acyclic_hierarchy p -> distinct _ (names p) -> sat_constr p (sty_field_rconstr (cl_dcl dcl') f' ty') = true -> 
  exists ty'', ftype p (cl_dcl dcl') f' = Some ty'' /\ sty_option p (Some ty'') (Some ty').
  intros p ty' dcl' f' Ord_p Distinct_Names Sat_Constr.
  inversion Sat_Constr as [H0]; destruct ty' as [cl'].
  destruct (ftype p (cl_dcl dcl') f') as [ ty' | ].
  exists ty'; split; auto.
  destruct ty' as [cl'']; destruct cl' as [dcl'' | ]; destruct cl'' as [dcl''' | ].
  destruct (in_path_In_path _ _ H0) as [cl'' [fds'' [mds'' H1]]].
  eapply sty_opt; eauto.
  eapply in_path_sty; eauto.
  discriminate.
  destruct (in_path_In_path _ _ H0) as [cl'' [fds'' [mds'' H1]]].
  eapply sty_opt; eauto.
  eapply sty_cl_object'; eauto; eapply In_p_In_names; eauto;
    eapply in_path_in_prog; eauto.
  eapply sty_opt; eauto; apply sty_opt_refl.
  destruct cl'; discriminate.
Qed.

Lemma sat_fieldw_constr : forall (p : P) (ty' : ty) (dcl' : dcl) (f' : f), 
  acyclic_hierarchy p -> distinct _ (names p) -> sat_constr p (sty_field_wconstr ty' (cl_dcl dcl') f' ) = true -> 
  exists ty'', ftype p (cl_dcl dcl') f' = Some ty'' /\ sty_option p (Some ty') (Some ty'').
  intros p ty' dcl' f' Ord_p Distinct_Names Sat_Constr.
  inversion Sat_Constr as [H0]; destruct ty' as [cl'].
  destruct (ftype p (cl_dcl dcl') f') as [ ty' | ].
  exists ty'; split; auto.
  destruct ty' as [cl'']; destruct cl' as [dcl'' | ]; destruct cl'' as [dcl''' | ].
  destruct (in_path_In_path _ _ H0) as [cl'' [fds'' [mds'' H1]]].
  eapply sty_opt; eauto; eapply in_path_sty; eauto.
  destruct (in_path_In_path _ _ H0) as [cl'' [fds'' [mds'' H1]]];
    eapply sty_opt; eauto.
  eapply sty_cl_object'; eauto. eapply In_p_In_names; eauto.
    eapply (in_path_in_prog p _ (cld_def dcl'' cl'' fds'' mds'')); eauto.
  discriminate.
  eapply sty_opt; eauto.
  apply sty_opt_refl.
  destruct cl'; discriminate.
Qed.

Lemma sat_meth_constr : forall (p : P) (dcl'': dcl) (cl' : cl) (m' : m) (ty_list : list ty),
  acyclic_hierarchy p -> distinct _ (names p) -> 
  sat_constr p (sty_meth_constr (cl_dcl dcl'') m' (ty_def cl') ty_list) = true ->
  exists ty'', exists ty_list', mtype p (cl_dcl dcl'') m' = Some (mty_def ty_list' ty'') /\
    sty_option p (Some ty'') (Some (ty_def cl')) /\ length ty_list = length ty_list' /\
    sty_opt_list (map (fun (y : ty*ty) => (p, Some (fst y), Some (snd y))) (combine ty_list ty_list')).
  intros p dcl' cl' m' ty_list Ord_p Distinct_Names Sat_Constr.
  inversion Sat_Constr as [H0].
  destruct (mtype p (cl_dcl dcl') m').
  destruct m as [ty_list' ty''].
  exists ty''; exists ty_list'; repeat split; auto.
  revert H0; case (eq_nat_dec (length ty_list) (length ty_list')); intros.
  destruct ty'' as [cl'']; destruct cl' as [dcl'' | ]; destruct cl'' as [dcl''' | ].
  destruct (andb_prop _ _ H0) as [In_path_dcl FoldR_T]; clear H0.
  destruct (in_path_In_path  _ _ In_path_dcl) as [cl'' [fds'' [mds'' In_path]]].
  eapply sty_opt; auto.
  eapply in_path_sty; eauto.
  discriminate.
  destruct (andb_prop _ _ H0) as [In_path_dcl FoldR_T]; clear H0.
  destruct (in_path_In_path  _ _ In_path_dcl) as [cl'' [fds'' [mds'' In_path]]].
  eapply sty_opt; auto.
  eapply sty_cl_object'; eauto; eapply In_p_In_names; eapply in_path_in_prog; eauto.
  eapply sty_opt; eauto; apply sty_opt_refl.
  destruct ty'' as [cl'']; destruct cl'' as [dcl'' | ]; destruct cl' as [dcl''' | ]; discriminate.
  revert H0; case (eq_nat_dec (length ty_list) (length ty_list')); intros e H0.
  exact e.
  destruct ty'' as [cl'']; destruct cl'' as [dcl'' | ]; destruct cl' as [dcl''' | ]; discriminate.
  destruct ty'' as [cl'']; destruct cl'' as [dcl'' | ]; destruct cl' as [dcl''' | ]; try discriminate.
  revert H0; case (eq_nat_dec (length ty_list) (length ty_list')); intros e H0.
  destruct (andb_prop _ _ H0) as [In_path_dcl FoldR_T]; clear H0.
  generalize ty_list ty_list' e Ord_p Distinct_Names FoldR_T; clear; induction ty_list; simpl; intros.
  constructor.
  destruct ty_list' as [| a' ty_list'].
  simpl in e; discriminate.
  simpl; simpl in FoldR_T; destruct a as [cl']; destruct a' as [cl''].
  destruct cl' as [dcl' | ]; destruct cl'' as [dcl'' | ]; try discriminate;
    try (destruct (andb_prop _ _ FoldR_T) as [In_path_dcl FoldR_T']; clear FoldR_T).
  constructor; try constructor; try constructor; try constructor.
  destruct (in_path_In_path _ _ In_path_dcl) as [cl'' [fds'' [mds'' H1]]];
    eapply sty_opt; eauto; eapply in_path_sty; eauto.
  eapply IHty_list; eauto.
  repeat constructor.
  destruct (in_path_In_path _ _ In_path_dcl) as [cl'' [fds'' [mds'' H1]]];
    eapply sty_opt; eauto; eapply sty_cl_object'; eauto. eapply In_p_In_names; eauto.
    eapply (in_path_in_prog p _ (cld_def dcl' cl'' fds'' mds'')); eauto.
  eapply IHty_list; eauto.
  repeat constructor.
  eapply sty_opt; eauto; eapply sty_opt_refl.
  eapply IHty_list; eauto.
  discriminate.
  revert H0; case (eq_nat_dec (length ty_list) (length ty_list')); intros e H0.
  destruct (andb_prop _ _ H0) as [In_path_dcl FoldR_T]; clear H0.
  generalize ty_list ty_list' e Ord_p Distinct_Names FoldR_T; clear; induction ty_list; simpl; intros.
  constructor.
  destruct ty_list' as [| a' ty_list'].
  simpl in e; discriminate.
  simpl; simpl in FoldR_T; destruct a as [cl']; destruct a' as [cl''].
  destruct cl' as [dcl' | ]; destruct cl'' as [dcl'' | ]; try discriminate;
    try (destruct (andb_prop _ _ FoldR_T) as [In_path_dcl FoldR_T']; clear FoldR_T).
  constructor; try constructor; try constructor; try constructor.
  destruct (in_path_In_path _ _ In_path_dcl) as [cl'' [fds'' [mds'' H1]]];
    eapply sty_opt; eauto; eapply in_path_sty; eauto.
  eapply IHty_list; eauto.
  repeat constructor.
  destruct (in_path_In_path _ _ In_path_dcl) as [cl'' [fds'' [mds'' H1]]];
    eapply sty_opt; eauto; eapply sty_cl_object'; eauto. eapply In_p_In_names; eauto.
    eapply (in_path_in_prog p _ (cld_def dcl' cl'' fds'' mds'')); eauto.
  eapply IHty_list; eauto.
  repeat constructor.
  eapply sty_opt; eauto; eapply sty_opt_refl.
  eapply IHty_list; eauto.
  discriminate.
  revert H0; case (eq_nat_dec (length ty_list) (length ty_list')); intros e H0.
  generalize ty_list ty_list' e Ord_p Distinct_Names H0; clear; induction ty_list; simpl; intros.
  constructor.
  destruct ty_list' as [| a' ty_list'].
  simpl in e; discriminate.
  simpl; simpl in H0; destruct a as [cl']; destruct a' as [cl''].
  destruct cl' as [dcl' | ]; destruct cl'' as [dcl'' | ]; try discriminate;
    try (destruct (andb_prop _ _ H0) as [In_path_dcl FoldR_T']; clear H0).
  constructor; try constructor; try constructor; try constructor.
  destruct (in_path_In_path _ _ In_path_dcl) as [cl'' [fds'' [mds'' H1]]];
    eapply sty_opt; eauto; eapply in_path_sty; eauto.
  eapply IHty_list; eauto.
  repeat constructor.
  destruct (in_path_In_path _ _ In_path_dcl) as [cl'' [fds'' [mds'' H1]]];
    eapply sty_opt; eauto; eapply sty_cl_object'; eauto. eapply In_p_In_names; eauto.
    eapply (in_path_in_prog p _ (cld_def dcl' cl'' fds'' mds'')); eauto.
  eapply IHty_list; eauto.
  repeat constructor.
  eapply sty_opt; eauto; eapply sty_opt_refl.
  eapply IHty_list; eauto.
  discriminate.
  discriminate.
Qed.

Lemma sat_cl_constr : forall (p : P) (ty' ty'': ty),
  acyclic_hierarchy p -> distinct _ (names p) -> (sat_constr p (sty_cl_constr ty' ty'') = true <-> 
  sty_option p (Some ty') (Some ty'')).
  intros p ty' ty'' Ord_p Distinct_Names; pa. 
  intros Sat_Constr; inversion Sat_Constr as [In_path_dcl].
  destruct ty' as [cl']; destruct ty'' as [cl'']; destruct cl' as [dcl' | ]; destruct cl'' as [dcl'' | ];
    try (destruct (in_path_In_path _ _ In_path_dcl) as [cl'' [fds'' [mds'' H1]]]);
      eapply sty_opt; eauto.
  eapply in_path_sty; auto; apply H1.
  eapply sty_cl_object'; eauto; eapply In_p_In_names; eauto;
    eapply (in_path_in_prog p _ (cld_def dcl' cl'' fds'' mds'')); eauto.
  rewrite path_cl_object in H1; simpl in H1; contradiction.
  apply sty_opt_refl.
  intros Sty_Opt; inversion Sty_Opt as [p' tyo tyo' ty1 ty2 H H0 Sty_One]; subst;
    inversion H; inversion H0; subst; clear H H0 Sty_Opt.
  destruct ty1 as [cl']; destruct ty2 as [cl'']; destruct cl' as [dcl' | ]; destruct cl'' as [dcl'' | ]; simpl.
  destruct (parent_in_path_sty' _ _ _ Ord_p Distinct_Names Sty_One) as [cl'' [fds'' [mds'' H1]]];
    eapply In_path_in_path; eauto.
  destruct (in_path_sty' _ _ _ Ord_p Distinct_Names Sty_One) as [cl'' [fds'' [mds'' H1]]];
    eapply In_path_in_path; eauto.
  generalize (sty_cl_object _ _ Sty_One); intros; discriminate.
  reflexivity.
Qed.

Lemma sat_if_constr : forall (p : P) (ty' ty'': ty),
  acyclic_hierarchy p -> distinct _ (names p) -> (sat_constr p (sty_if_constr ty' ty'') = true <-> 
  sty_option p (Some ty') (Some ty'') \/ sty_option p (Some ty'') (Some ty')).
  intros p ty' ty'' Ord_p Distinct_Names; pa. 
  intros Sat_Constr; inversion Sat_Constr as [In_path_dcl].
  destruct ty' as [cl']; destruct ty'' as [cl'']; destruct cl' as [dcl' | ]; destruct cl'' as [dcl'' | ];
    try (destruct (in_path_In_path _ _ In_path_dcl) as [cl'' [fds'' [mds'' H1]]]);
      try (destruct (orb_prop _ _ In_path_dcl) as [LIn_path | RIn_path]).
  destruct (in_path_In_path _ _ LIn_path) as [cl'' [fds'' [mds'' H1]]];
    left; eapply sty_opt; eauto; eapply in_path_sty; eauto.
  destruct (in_path_In_path _ _ RIn_path) as [cl'' [fds'' [mds'' H1]]];
    right; eapply sty_opt; eauto; eapply in_path_sty; eauto.
  left; eapply sty_opt; eauto; eapply sty_cl_object'; eauto; eapply In_p_In_names; eauto;
    eapply (in_path_in_prog p _ (cld_def dcl' cl'' fds'' mds'')); eauto.
  right; eapply sty_opt; eauto; eapply sty_cl_object'; eauto; eapply In_p_In_names; eauto;
    eapply (in_path_in_prog p _ (cld_def dcl'' cl'' fds'' mds'')); eauto.
  left; eapply sty_opt; eauto; apply sty_opt_refl.
  intros Sty_Opt; destruct Sty_Opt as [Sty_Opt | Sty_Opt];
    inversion Sty_Opt as [p' tyo tyo' ty1 ty2 H H0 Sty_One]; subst;
    inversion H; inversion H0; subst; clear H H0 Sty_Opt.
  destruct ty1 as [cl']; destruct ty2 as [cl'']; destruct cl' as [dcl' | ]; destruct cl'' as [dcl'' | ]; simpl.
  destruct (parent_in_path_sty' _ _ _ Ord_p Distinct_Names Sty_One) as [cl'' [fds'' [mds'' H1]]].
  rewrite (In_path_in_path _ _ _ _ _ H1); auto.
  destruct (in_path_sty' _ _ _ Ord_p Distinct_Names Sty_One) as [cl'' [fds'' [mds'' H1]]];
    eapply In_path_in_path; eauto.
  generalize (sty_cl_object _ _ Sty_One); intros; discriminate.
  reflexivity.
  destruct ty1 as [cl']; destruct ty2 as [cl'']; destruct cl' as [dcl' | ]; destruct cl'' as [dcl'' | ]; simpl.
  destruct (parent_in_path_sty' _ _ _ Ord_p Distinct_Names Sty_One) as [cl'' [fds'' [mds'' H1]]].
  rewrite (In_path_in_path _ _ _ _ _ H1); destruct (in_path (path p (cl_dcl dcl'')) dcl'); auto.
  destruct (in_path_sty' _ _ _ Ord_p Distinct_Names Sty_One) as [cl'' [fds'' [mds'' H1]]];
    eapply In_path_in_path; eauto.
  generalize (sty_cl_object _ _ Sty_One); intros; discriminate.
  reflexivity.
Qed.

Lemma sat_constr_wf : forall (g : G) (stmt_list : list_s) (p : P) (c_list : list ty_constraint), 
  wf_stmt_list_constr g stmt_list c_list -> sat_constr_list p c_list = true ->
  acyclic_hierarchy p -> distinct _ (names p) -> wf_stmt_list' p g stmt_list.
  intros g stmt_list p.
  elim stmt_list using s_list_ind with (P := fun s => forall c_list', acyclic_hierarchy p -> distinct _ (names p) ->
    wf_stmt_constr g s c_list' ->sat_constr_list p c_list' = true -> wf_stmt p g s);
     try (intros until c_list'; intros Ord_p Distinct_Names WF_stmt Sat_constr_list);
       try (inversion WF_stmt; subst; unfold sat_constr_list in Sat_constr_list; 
         destruct (andb_prop _ _ Sat_constr_list) as [Sat_constr Sat_Remain]; clear Sat_constr_list WF_stmt).
  constructor; rewrite H2; apply ((proj1 (sat_cl_constr _ _ _ Ord_p Distinct_Names) Sat_constr)); eauto.
  constructor; rewrite H1; rewrite H3; eapply (proj1 (sat_cl_constr _ _ _ Ord_p Distinct_Names)); eauto.
  destruct cl' as [dcl' | ].
  destruct (sat_fieldr_constr _ _ _ _ Ord_p Distinct_Names Sat_constr) as [f' [H1 H0]].
  eapply wf_field_read; eauto.
  rewrite H4; auto.
  destruct ty' as [cl']; destruct cl' as [dcl' | ]; simpl in Sat_constr;
    unfold ftype in Sat_constr; rewrite path_cl_object in Sat_constr; simpl in Sat_constr;
      discriminate.
  destruct cl' as [dcl' | ].
  destruct (sat_fieldw_constr _ _ _ _ Ord_p Distinct_Names Sat_constr) as [ty'' [H1 H0]].
  eapply wf_field_write; eauto.
  congruence.
  destruct ty' as [cl']; destruct cl' as [dcl' | ]; simpl in Sat_constr;
    unfold ftype in Sat_constr; rewrite path_cl_object in Sat_constr; simpl in Sat_constr;
      discriminate.
  destruct cl' as [dcl' | ]; destruct ty' as [cl''].
  destruct (sat_meth_constr _ _ _ _ _ Ord_p Distinct_Names Sat_constr) as [ty'' [ty_list' [H [H0 [H1 H3]]]]].
  rewrite <- (spurious_map_fst l ty_list').
  eapply wf_mcall; eauto.
  rewrite spurious_map_snd; eauto.
  rewrite <- H1; generalize ty_list H6; clear; induction l; simpl; auto;
    intros ty_list H.
  inversion H; subst; auto.
  destruct (XMap.find a g).
  destruct (fold_right
          (fun (y : x) (m : option (list ty)) =>
           match XMap.find (elt:=ty) y g with
           | Some ty' =>
               match m with
               | Some m' => Some (ty' :: m')
               | None => None
               end
           | None => None
           end) (Some nil) l); inversion H; subst; simpl; auto.
  discriminate.
  generalize l ty_list ty_list' H6 H3 H1; clear; induction l; intros.
  simpl; constructor.
  destruct ty_list'; simpl.
  constructor.
  simpl in H6; destruct (XMap.find (elt:=ty) a g); 
    destruct (         fold_right
           (fun (y : x) (m : option (list ty)) =>
            match XMap.find (elt:=ty) y g with
            | Some ty' =>
                match m with
                | Some m' => Some (ty' :: m')
                | None => None
                end
            | None => None
            end) (Some nil) l).
  inversion H6; subst; inversion H3; subst; auto.
  constructor; eauto.
  discriminate.
  discriminate.
  discriminate.
  rewrite H5; auto.
  rewrite <- H1; generalize ty_list H6; clear; induction l; simpl; auto;
    intros ty_list H.
  inversion H; subst; auto.
  destruct (XMap.find (elt:=ty) a g); 
    destruct (         fold_right
           (fun (y : x) (m : option (list ty)) =>
            match XMap.find (elt:=ty) y g with
            | Some ty' =>
                match m with
                | Some m' => Some (ty' :: m')
                | None => None
                end
            | None => None
            end) (Some nil) l); simpl in H; try discriminate.
  simpl in H; inversion H; simpl; rewrite (IHl l0); reflexivity.
  simpl in Sat_constr.
  unfold mtype in Sat_constr; unfold get_md in Sat_constr; rewrite path_cl_object in Sat_constr;
    simpl in Sat_constr; discriminate.
  constructor; auto.
  rewrite H5; rewrite H7; applyI (sat_if_constr _ ty' ty'' Ord_p Distinct_Names).
  eapply H; eauto; destruct (sat_constr_list_app _ _ _ Sat_Remain); auto.
  eapply H0; eauto; destruct (sat_constr_list_app _ _ _ Sat_Remain); auto.
  constructor; applyI wf_stmt_list'_iff; eapply H; eauto.
  inversion WF_stmt; auto.
  intros; constructor.
  intros; inversion H1; subst; destruct (sat_constr_list_app _ _ _ H2).
  constructor.
  eapply H; eauto.
  eapply H0; eauto.
Qed.

Lemma sat_fieldr_constr' : forall (p : P) (ty' ty'' : ty) (dcl' : dcl) (f' : f), 
  acyclic_hierarchy p -> distinct _ (names p) -> ftype p (cl_dcl dcl') f' = Some ty'' -> 
  sty_option p (Some ty'') (Some ty') -> sat_constr p (sty_field_rconstr (cl_dcl dcl') f' ty') = true.
  intros p ty' ty'' dcl' f' Ord_p Distinct_Names FType Sty_Opt; simpl.
  destruct ty' as [cl']; rewrite FType.
  destruct cl' as [dcl'' | ]; destruct ty'' as [cl'']; destruct cl'' as [dcl''' |]; auto.
  eapply in_path_sty_option'; auto.
  elimtype False; eapply Not_sty_cl_object_dcl; eauto.
  eapply sty_option_in_path_self; eauto.
Qed.

Lemma sat_fieldw_constr' : forall (p : P) (ty' ty'': ty) (dcl' : dcl) (f' : f), 
  acyclic_hierarchy p -> distinct _ (names p) -> ftype p (cl_dcl dcl') f' = Some ty'' ->
  sty_option p (Some ty') (Some ty'') -> sat_constr p (sty_field_wconstr ty' (cl_dcl dcl') f' ) = true.
  intros p ty' ty'' dcl' f' Ord_p Distinct_Names FType Sty_Opt; simpl;
    destruct ty' as [cl']; rewrite FType.
  destruct cl' as [dcl'' | ]; destruct ty'' as [cl'']; destruct cl'' as [dcl''' |]; auto.
  eapply in_path_sty_option'; auto.
  eapply sty_option_in_path_self; eauto.
  elimtype False; eapply Not_sty_cl_object_dcl; eauto.
Qed.

Lemma sat_meth_constr' : forall (p : P) (dcl'': dcl) (cl' : cl) (ty'' : ty) (m' : m) (ty_list ty_list': list ty),
  acyclic_hierarchy p -> distinct _ (names p) -> 
  mtype p (cl_dcl dcl'') m' = Some (mty_def ty_list' ty'') ->
  sty_option p (Some ty'') (Some (ty_def cl')) -> length ty_list = length ty_list' ->
  sty_opt_list (map (fun (y : ty*ty) => (p, Some (fst y), Some (snd y))) (combine ty_list ty_list')) ->
    sat_constr p (sty_meth_constr (cl_dcl dcl'') m' (ty_def cl') ty_list) = true.
  intros p dcl' cl' ty' m' ty_list ty_list' Ord_p Distinct_Names MType Sty_Opt Len_tyl' Sty_Opt_List.
  simpl; rewrite MType.
  destruct ty' as [cl''].
  destruct cl'' as [dcl'' | ]; destruct cl' as [dcl''' | ]; 
    try (rewrite Len_tyl'; case (eq_nat_dec (length ty_list') (length ty_list')); try congruence; 
      intros; clear e).
  rewrite in_path_sty_option'; auto; simpl.
  revert Distinct_Names Ord_p Sty_Opt_List; clear; induction (combine ty_list ty_list'); simpl; intros.
  reflexivity.
  destruct a as [ty' ty'']; destruct ty' as [cl']; destruct ty'' as [cl'']; inversion Sty_Opt_List; subst;
    destruct cl' as [dcl' | ]; destruct cl'' as [dcl'' | ]; simpl in Sty_Opt_List; 
      try rewrite IHl; auto.
  rewrite in_path_sty_option'; simpl; auto; reflexivity.
  erewrite sty_option_in_path_self; eauto.
  elimtype False; eapply Not_sty_cl_object_dcl; eauto.
  erewrite sty_option_in_path_self; simpl; auto.
  revert Distinct_Names Ord_p Sty_Opt_List; clear; induction (combine ty_list ty_list'); simpl; intros.
  reflexivity.
  destruct a as [ty' ty'']; destruct ty' as [cl']; destruct ty'' as [cl'']; inversion Sty_Opt_List; subst;
    destruct cl' as [dcl' | ]; destruct cl'' as [dcl'' | ]; simpl in Sty_Opt_List; 
      try rewrite IHl; auto.
  rewrite in_path_sty_option'; simpl; auto; reflexivity.
  erewrite sty_option_in_path_self; eauto.
  elimtype False; eapply Not_sty_cl_object_dcl; eauto.  
  apply Sty_Opt.
  elimtype False; eapply Not_sty_cl_object_dcl; eauto.  
  revert Distinct_Names Ord_p Sty_Opt_List; clear; induction (combine ty_list ty_list'); simpl; intros.
  reflexivity.
  destruct a as [ty' ty'']; destruct ty' as [cl']; destruct ty'' as [cl'']; inversion Sty_Opt_List; subst;
    destruct cl' as [dcl' | ]; destruct cl'' as [dcl'' | ]; simpl in Sty_Opt_List; 
      try rewrite IHl; auto.
  rewrite in_path_sty_option'; simpl; auto; reflexivity.
  erewrite sty_option_in_path_self; eauto.
  elimtype False; eapply Not_sty_cl_object_dcl; eauto.  
Qed.

Lemma sat_constr_wf' : forall (g : G) (stmt_list : list_s) (p : P), 
  acyclic_hierarchy p -> distinct _ (names p) -> wf_stmt_list' p g stmt_list -> 
  (exists c_list, wf_stmt_list_constr g stmt_list c_list /\ sat_constr_list p c_list = true).
  intros g stmt_list p.
  elim stmt_list using s_list_ind with (P := fun s => acyclic_hierarchy p -> distinct _ (names p) ->
    wf_stmt p g s -> (exists c_list', wf_stmt_constr g s c_list' /\ sat_constr_list p c_list' = true)).
  intros var cl' Ord_p Distinct_Names WF_Stmt; inversion WF_Stmt; inversion H2; subst;
    exists (sty_cl_constr (ty_def cl') ty' :: nil); split.
  constructor; auto.
  unfold sat_constr_list; rewrite H5 in H2; rewrite (proj2 (sat_cl_constr _ _ _ Ord_p Distinct_Names) H2); 
    simpl; reflexivity.
  intros var x Ord_p Distinct_Names WF_Stmt; inversion WF_Stmt; inversion H2; subst;
    exists (sty_cl_constr ty5 ty' :: nil); split.
  constructor; auto.
  unfold sat_constr_list; rewrite H5, H4 in H2; rewrite (proj2 (sat_cl_constr _ _ _ Ord_p Distinct_Names) H2); 
    simpl; reflexivity.
  intros var x f Ord_p Distinct_Names WF_Stmt; inversion WF_Stmt; inversion H6; subst;
    destruct cl5 as [dcl' | ].
  exists (sty_field_rconstr (cl_dcl dcl') f ty' :: nil); split.
  constructor; auto.
  unfold sat_constr_list; rewrite H8 in H6; rewrite (sat_fieldr_constr' _ _ _ _ _ Ord_p Distinct_Names);
    simpl; eauto.
  unfold ftype in H5; rewrite path_cl_object in H5; simpl in H5; discriminate.
  intros x' y f Ord_p Distinct_Names WF_Stmt; inversion WF_Stmt; inversion H6; subst;
    destruct cl5 as [dcl' | ]; rewrite H7 in H6.
  exists (sty_field_wconstr ty0 (cl_dcl dcl') f :: nil); split.
  constructor; auto.
  unfold sat_constr_list; erewrite sat_fieldw_constr'; eauto.
  unfold ftype in H5; rewrite path_cl_object in H5; simpl in H5; discriminate.
  intros var x' m l Ord_p Distinct_Names WF_Stmt; inversion WF_Stmt; inversion H8;
    subst; destruct cl5 as [dcl' | ].
  exists (sty_meth_constr (cl_dcl dcl') m ty'0 (map (fun y : x * ty => match (XMap.find (elt:=ty) (fst y) g) with 
                                                                         Some ty' => ty' 
                                                                         | _ => ty_def cl_object end) y_ty_list) :: nil); split.
  constructor; auto.
  generalize H7; clear; induction y_ty_list; simpl; intros; auto; simpl in H7; inversion H7; subst.
  inversion H1; subst; rewrite H; rewrite IHy_ty_list; auto.
  destruct ty'0; unfold sat_constr_list; erewrite sat_meth_constr'; eauto.
  inversion H9; subst; eapply sty_opt; eauto.
  clear; induction y_ty_list; simpl; auto.
  revert H7; clear; induction y_ty_list; simpl; intros; auto.
  constructor; try (constructor; constructor; constructor).
  inversion H7; subst; destruct (XMap.find (fst a) g); auto; inversion H1; discriminate.
  apply IHy_ty_list; inversion H7; subst; auto.
  unfold mtype in H6; unfold get_md in H6; rewrite path_cl_object in H6; simpl in H6; discriminate.
  intros x' y s1 s2 IHs1 IHs2 Ord_p Distinct_Names WF_Stmt; inversion WF_Stmt; subst;
    destruct (IHs1 Ord_p Distinct_Names H6) as [c_list1 [WF_Constr1 Sat_Constr1]];
      destruct (IHs2 Ord_p Distinct_Names H7) as [c_list2 [WF_Constr2 Sat_Constr2]];
        destruct H4 as [H4 | H4]; inversion H4; subst.
  exists (sty_if_constr ty5 ty' :: c_list1 ++ c_list2); split;
    try (constructor; auto); unfold sat_constr_list; fold (sat_constr_list p (c_list1 ++ c_list2));
      try (rewrite sat_constr_list_app'); auto;
        rewrite (proj2 (sat_if_constr _ ty5 ty' Ord_p Distinct_Names)); auto;
          left; congruence.
  exists (sty_if_constr ty' ty5 :: c_list1 ++ c_list2); split;
    try (constructor; auto); unfold sat_constr_list; fold (sat_constr_list p (c_list1 ++ c_list2));
      try (rewrite sat_constr_list_app'); auto;
        rewrite (proj2 (sat_if_constr _ ty' ty5 Ord_p Distinct_Names)); auto;
          right; congruence.  
  intros l IHl Ord_p Distinct_Names WF_Stmt; inversion WF_Stmt; subst;
    destruct (IHl Ord_p Distinct_Names ((proj1 (wf_stmt_list'_iff _ _ _)) H2)) as [c_list' [WF_constr Sat_Constr]];
      exists c_list'; split; try constructor; auto.
  intros Ord_p Distinct_Names WF_Stmt.
  exists nil; repeat constructor; auto.
  intros l s IHs IHl Ord_p Distinct_Names WF_Stmt; inversion WF_Stmt; subst.
    destruct (IHs Ord_p Distinct_Names H3) as [c_list1 [WF_constr1 Sat_Constr1]];
      destruct (IHl Ord_p Distinct_Names H4) as [c_list2 [WF_constr2 Sat_Constr2]];
      exists (c_list1 ++ c_list2); split; try constructor; auto.
    apply sat_constr_list_app'; auto.
Qed.

Lemma sat_in_prog_constr : forall (cl' : cl) (p : P),
  sat_constr p (in_prog_constr cl') = true <-> In cl' (names p).
  simpl; intros; split; intros; destruct cl' as [dcl' |]; simpl.
  destruct (in_path_In_path _ _ H) as [cl' [fds' [mds' H0]]]; eapply In_p_In_names; eauto.
  induction p; simpl; auto; destruct a; simpl; right; auto.
  destruct (In_names_In_p _ _ H) as [cl' [fds' [mds' H0]]]; eapply In_path_in_path; apply H0.
  induction p; simpl; auto; destruct a; simpl; right; auto.
Qed.

Lemma sat_constr_wf_meth : forall (ty' : ty) (md' : md) (c_list : list ty_constraint) (p : P), 
  acyclic_hierarchy p -> distinct _ (names p) -> 
  wf_meth_constr ty' md' c_list -> sat_constr_list p c_list = true ->
  wf_meth p ty' md'.
  intros ty' md' c_list p Ord_p Distinct_Names WF_Meth_Constr Sat_Constr.
  inversion WF_Meth_Constr; subst; destruct ty' as [cl'];
    destruct (vd_list_decomp vd_list) as [ty_list' [var_list' Ty_Var_eq]]; rewrite Ty_Var_eq;
      rewrite <- (unmake_make_s_list_idem s_list).
  eapply wf_method; eauto.
  inversion Sat_Constr; clear Sat_Constr; subst; destruct (andb_prop _ _ H3) as [Sat_Constr1 Sat_Constr2].
  destruct (sat_constr_list_app _ _ _ Sat_Constr2).
  generalize H0; clear; induction (combine ty_list' var_list'); simpl; intros; constructor;
    destruct (andb_prop _ _ H0) as [H1 H2].
  destruct a as [ty' var']; simpl in *|-*; destruct ty' as [cl'].
  eapply wf_valid_dcl.
  applyI sat_in_prog_constr.
  apply IHl; auto.
  generalize H; rewrite Ty_Var_eq; clear; induction (combine ty_list' var_list'); simpl; auto.
  intros; split; destruct H as [H0 H1].
  generalize H0; clear; induction l; simpl; auto.
  unfold not; intros; destruct H as [LH | RH].
  apply H0; left; congruence.
  apply IHl; auto.
  auto.
  inversion Sat_Constr; clear Sat_Constr; subst; destruct (andb_prop _ _ H3) as [Sat_Constr1 Sat_Constr2];
    destruct (sat_constr_list_app _ _ _ Sat_Constr2).
  applyI wf_stmt_list'_iff; apply sat_constr_wf with (c_list := c_list0); auto; simpl; 
    rewrite spurious_map_vd_reverse in H1; exact H1.
  inversion Sat_Constr; clear Sat_Constr; subst; destruct (andb_prop _ _ H3) as [Sat_Constr1 Sat_Constr2].
  simpl; rewrite spurious_map_vd_reverse in H2; rewrite H2;
    eapply (proj1 (sat_cl_constr _ _ _ Ord_p Distinct_Names)); simpl; auto.
Qed.

Lemma sat_constr_wf_meth' : forall (ty' : ty) (md' : md) (p : P), 
  acyclic_hierarchy p -> distinct _ (names p) ->   wf_meth p ty' md' ->
  exists c_list, wf_meth_constr ty' md' c_list /\ sat_constr_list p c_list = true.
  intros ty' md' p Ord_p Distinct_Names WF_Meth.
  inversion WF_Meth; subst.
  destruct (sat_constr_wf' _ _ _ Ord_p Distinct_Names ((proj1 (wf_stmt_list'_iff _ _ _)) H2))
    as [clist' [WF_Stmt_Constr Sat_Stmt_Constr]].
  inversion H3; subst.
  exists (sty_cl_constr ty5 ty_5 :: map
    (fun vd' : vd =>
      match vd' with
        | vd_def (ty_def cl') _ => in_prog_constr cl'
      end) (map (fun ty_var : ty * var => vd_def (fst ty_var) (snd ty_var)) ty_var_list)  ++ clist'); split.
  eapply wf_method_constr; eauto.
  generalize H0; clear; induction ty_var_list; auto; destruct a; simpl; intros H; destruct H as [LH RH]; split; auto;
    generalize LH; clear; induction ty_var_list; auto; destruct a; simpl; auto; unfold not; intros H H0; 
      destruct H0 as [Eq | In]; auto; apply IHty_var_list; auto.
  simpl in WF_Stmt_Constr; rewrite make_unmake_s_list_idem; rewrite spurious_map_vd_reverse; auto.
  simpl in H1; rewrite spurious_map_vd_reverse; auto.
  simpl; apply andb_true_intro; split.
  destruct ty5 as [cl']; destruct ty_5 as [cl'']; destruct cl' as [dcl' |]; destruct cl'' as [dcl'' |]; auto.
  inversion H4; subst; destruct (parent_in_path_sty' _ _ _ Ord_p Distinct_Names H5) as [cl' [fds' [mds' In_cld]]];
      eapply In_path_in_path; apply In_cld.
  rewrite H1 in H3; eapply sty_option_in_path_self; eauto.
  rewrite H1 in H3; elimtype False; eapply Not_sty_cl_object_dcl; eauto.  
  eapply sat_constr_list_app'; split.
  generalize H; clear; induction ty_var_list; simpl; try reflexivity; destruct a; simpl; intros WF_TypeL.
  inversion WF_TypeL; subst; apply andb_true_intro; split; auto.
  destruct t as [cl']; inversion H1; subst; simpl; destruct cl' as [dcl' |]; auto.
  destruct (In_names_In_p _ _ H2) as [cl' [fds' [mds' In_cld]]]; eapply In_path_in_path; apply In_cld.
  auto.
Qed.

Lemma sat_constr_wf_cld : forall (cld' : cld) (c_list : list ty_constraint) (p : P), 
  acyclic_hierarchy p -> distinct _ (names p) -> 
  wf_cld_constr cld' c_list -> sat_constr_list p c_list = true ->
  wf_class p cld'.
  intros cld' c_list p Ord_p Distinct_Names WF_Cld_Constr Sat_Constr; 
    inversion WF_Cld_Constr; subst; simpl in *|-*.
  destruct (andb_prop _ _ Sat_Constr) as [In_Path_Dcl' Sat_ConstrR]; 
    destruct (andb_prop _ _ Sat_ConstrR) as [List_Inter Sat_ConstrR1]; 
      destruct (andb_prop _ _ Sat_ConstrR1) as [Distinct_MType Sat_ConstrR''];
        destruct (sat_constr_list_app _ _ _ Sat_ConstrR'') as [WF_Fds Sat_Meth_Constr];
          clear Sat_ConstrR Sat_ConstrR1 Sat_ConstrR'' Sat_Constr.
  eapply wf_cl; eauto.
  constructor; destruct (in_path_In_path _ _ In_Path_Dcl') as [cl' [fds' [mds' H0]]]; 
    eapply In_p_In_names; eauto.
  congruence.
  apply fds_map_idem.
  generalize H2; clear; induction fds; simpl; auto; destruct a; intros;
    destruct H2 as [In_f Distinct_fds]; split; auto.
  unfold not; intros; apply In_f; simpl in H; generalize H; clear; induction fds; 
    simpl; auto; destruct a; simpl; intros H; destruct H as [Eq | In]; auto.
  generalize List_Inter; clear; induction fds; simpl; auto; destruct a; simpl;
    destruct (in_nat_list f (fields p (cl_dcl dcl''))); simpl; intros;
      auto; discriminate.
  generalize WF_Fds Ord_p Distinct_Names; clear; induction fds; simpl; constructor;
    destruct a; simpl; destruct t as [cl']; destruct (andb_prop _ _ WF_Fds) as [H H0];
      auto; destruct cl' as [dcl' | ]; constructor; simpl in H; try apply cl_object_in_names;
        destruct (in_path_In_path _ _ H) as [cl' [fds' [mds' H1]]]; eapply In_p_In_names; 
          eauto.
  generalize c_list0 Ord_p Distinct_Names H4 Sat_Meth_Constr; clear; induction mds; simpl; intros;
    auto; inversion H4; subst; constructor; auto;
      destruct (sat_constr_list_app _ _ _ Sat_Meth_Constr) as [Sat_Meth_Constr' Sat_Mds_Constr];
        eauto; eapply sat_constr_wf_meth; eauto.
  generalize Distinct_MType; clear; induction mds; simpl; intros; try contradiction;
    destruct H as [Eq | In]; subst. 
  rewrite ((proj2 (not_in_list_In_list _ _)) H0) in Distinct_MType; 
    simpl in Distinct_MType; destruct (mtype p (cl_dcl dcl'') m'); try discriminate;
      destruct (andb_prop _ _ Distinct_MType) as [MType1 MType2];
        apply sym_eq; rewrite (proj1 (eq_mty_eq _ _)); eauto.
  destruct a as [ty'' m'']; destruct ty'' as [cl'']; 
    destruct (not_in_list m (methods p (cl_dcl dcl''))); simpl in Distinct_MType;
      eapply IHmds; eauto.
  simpl in Distinct_MType; destruct (mtype p (cl_dcl dcl'') m); try discriminate;
    destruct (andb_prop _ _ Distinct_MType) as [MType1 MType2]; eauto.
  destruct (sat_constr_list_app _ _ _ Sat_Constr) as [WF_Fds Sat_Meth_Constr];
    clear Sat_Constr.
  eapply wf_cl; eauto.
  constructor; apply cl_object_in_names.
  congruence.
  apply fds_map_idem.
  generalize H1; clear; induction fds; simpl; auto; destruct a; intros;
    destruct H1 as [In_f Distinct_fds]; split; auto.
  unfold not; intros; apply In_f; simpl in H; generalize H; clear; induction fds; 
    simpl; auto; destruct a; simpl; intros H; destruct H as [Eq | In]; auto.
  unfold fields; rewrite path_cl_object; simpl; clear; induction fds; simpl; auto.
  generalize WF_Fds Ord_p Distinct_Names; clear; induction fds; simpl; constructor;
    destruct a; simpl; destruct t as [cl']; destruct (andb_prop _ _ WF_Fds) as [H H0];
      auto; destruct cl' as [dcl' | ]; constructor; simpl in H; try apply cl_object_in_names;
        destruct (in_path_In_path _ _ H) as [cl' [fds' [mds' H1]]]; eapply In_p_In_names; 
          eauto.
  generalize c_list0 Ord_p Distinct_Names H3 Sat_Meth_Constr; clear; induction mds; simpl; intros;
    auto; inversion H3; subst; constructor; auto;
      destruct (sat_constr_list_app _ _ _ Sat_Meth_Constr) as [Sat_Meth_Constr' Sat_Mds_Constr];
        eauto; eapply sat_constr_wf_meth; eauto.
  unfold methods; rewrite path_cl_object; simpl; auto; intros; contradiction.
Qed.

Lemma sat_constr_wf_meth_list : forall (ty' : ty) (mds : list md) (p : P),
  acyclic_hierarchy p -> distinct _ (names p) ->
  wf_meth_list (map (fun md' : md => (p, ty', md')) mds) ->
  exists c_list, wf_meth_list_constr ty' mds c_list /\ sat_constr_list p c_list = true.
  intros ty' mds p Ord_p Distinct_Names WF_Meth_list; induction mds; inversion WF_Meth_list; subst.
  exists nil; simpl; split; auto; constructor.
  destruct (IHmds H4) as [c_list1 [WF_Meth_list' Sat_Constr1]];
    destruct (sat_constr_wf_meth' _ _ _ Ord_p Distinct_Names H1) as [c_list2 [WF_Meth_Constr Sat_Constr2]];
      exists (c_list2 ++ c_list1); split.
  constructor; auto.
  apply sat_constr_list_app'; split; auto.
Qed.

Lemma sat_constr_wf_cld' : forall (cld' : cld) (p : P), 
  acyclic_hierarchy p -> distinct _ (names p) -> wf_class p cld' ->
  exists c_list, wf_cld_constr cld' c_list /\ sat_constr_list p c_list = true.
  intros cld' p Ord_p Distinct_Names WF_Cld; inversion WF_Cld as [ty_f_list md_list p' dcl' cl' fds' 
    WF_Type_cl' Neq_cl' Eq_fds' Distinct_f List_Inter WF_TyL WF_Meth Distinct_m Inherited_mds]; subst;
  destruct (sat_constr_wf_meth_list _ _ _ Ord_p Distinct_Names WF_Meth) as [c_list' [WF_Meth_Constr Sat_Meth_Constr]]; 
    destruct cl' as [dcl'' |].
  exists (in_prog_constr (cl_dcl dcl'')
    :: inherited_fields_constr
    (map (fun fd' : fd => match fd' with
                            | fd_def _ f' => f'
                          end)
    (map (fun tyf : ty * f => fd_def (fst tyf) (snd tyf)) ty_f_list))
    (cl_dcl dcl'')
    :: inherited_methods_constr md_list (cl_dcl dcl'')
    :: map
    (fun fd' : fd =>
      match fd' with
        | fd_def (ty_def cl') _ => in_prog_constr cl'
      end)
    (map (fun tyf : ty * f => fd_def (fst tyf) (snd tyf))
      ty_f_list) ++ c_list'); split.
  eapply wf_class_constraint; eauto.
  generalize Distinct_f; clear; induction ty_f_list; simpl; auto; unfold not; intros; 
    destruct Distinct_f as [Not_In Distinct]; split; auto; generalize Not_In; clear; induction ty_f_list; 
      simpl; auto; intros Not_In In_a; destruct a; destruct In_a as [Eq_a | In_a']; auto.
  simpl; repeat (apply andb_true_intro; split).
  inversion WF_Type_cl'; subst; destruct (In_names_In_p _ _ H1) as [cl' [fds' [mds' In_p]]]; eapply In_path_in_path; eauto.
  generalize List_Inter; clear; induction ty_f_list; simpl; auto; destruct a; simpl;
    destruct (in_nat_list f (fields p (cl_dcl dcl''))); simpl; intros; try discriminate;
      rewrite IHty_f_list; auto.
  generalize Inherited_mds; clear; induction md_list; simpl; intros; auto;
    destruct a; destruct m; simpl; caseEq (not_in_list m (methods p (cl_dcl dcl''))); simpl; intros.
  rewrite IHmd_list; auto; intros; eapply Inherited_mds; eauto.
  erewrite <- Inherited_mds; eauto.
  apply andb_true_intro; split.
  unfold get_vdstys; apply (proj2 (eq_mty_eq _ _)); reflexivity.
  rewrite IHmd_list; auto; intros; eapply Inherited_mds; eauto.
  apply ((proj1 (not_in_list_In_list _ _)) H).
  apply sat_constr_list_app'; split; auto.
  generalize WF_TyL; clear; induction ty_f_list; simpl; auto; intros; inversion WF_TyL; subst;
    apply andb_true_intro; split; auto.
  destruct a; destruct t; inversion H1; subst; destruct c; simpl; try apply (in_names_cl_object); auto;
    destruct (In_names_In_p _ _ H2) as [cl' [fds' [mds' In_p]]]; eapply In_path_in_path; eauto.
  exists (map (fun fd' : fd =>
    match fd' with
      | fd_def (ty_def cl') _ =>
        in_prog_constr cl'
    end) _ ++ c_list'); split.
  eapply wf_class_constraint_obj; eauto.
  generalize Distinct_f; clear; induction ty_f_list; simpl; auto; unfold not; intros; 
    destruct Distinct_f as [Not_In Distinct]; split; auto; generalize Not_In; clear; induction ty_f_list; 
      simpl; auto; intros Not_In In_a; destruct a; destruct In_a as [Eq_a | In_a']; auto.
  apply sat_constr_list_app'; split; auto.
  generalize WF_TyL; clear; induction ty_f_list; simpl; auto; intros; inversion WF_TyL; subst;
    apply andb_true_intro; split; auto.
  destruct a; destruct t; inversion H1; subst; destruct c; simpl; try apply (in_names_cl_object); auto;
    destruct (In_names_In_p _ _ H2) as [cl' [fds' [mds' In_p]]]; eapply In_path_in_path; eauto.
Qed.

Lemma sat_constr_wf_cld_list : forall (clds : list cld) (p : P) (c_list : list ty_constraint),
  acyclic_hierarchy p -> acyclic_hierarchy clds -> distinct _ (names p) ->
  wf_cld_constr_list clds c_list -> sat_constr_list p c_list = true ->
  wf_class_list (map (fun cld_ : cld => (p, cld_)) clds).
  induction clds; simpl; intros p c_list Ord_p Ord_clds Distinct_Names WF_CldL Sat_Constr; constructor;
    inversion WF_CldL as [| cld' p' c_list1 c_list2 WF_a_Constr WF_CldL']; subst; 
      destruct (sat_constr_list_app _ _ _ Sat_Constr) as [Sat_Constr1 Sat_Constr2].
  eapply sat_constr_wf_cld; eauto.
  inversion Ord_clds; eauto.
  inversion Ord_clds as [| p' cld' Ord_clds' Ex_Parent]; destruct Ex_Parent as [cl' [Get_Parent_a In_cl']]; 
    subst; exists (get_parent a); split; auto; generalize In_cl'; clear; induction clds; simpl; auto; 
      destruct a0; simpl; intros; destruct In_cl' as [Eq_a | In_a]; auto.
Qed.
  
Lemma sat_constr_wf_cld_list' : forall (clds : list cld) (p : P),
  acyclic_hierarchy p -> distinct _ (names p) -> wf_class_list (map (fun cld_ : cld => (p, cld_)) clds) ->
  exists c_list, wf_cld_constr_list clds c_list /\ sat_constr_list p c_list = true.
  induction clds; simpl; intros p Ord_p Distinct_Names WF_CldL.
  exists nil; simpl; repeat split; try constructor.
  inversion WF_CldL as [| p' cld' clds' WF_cld' WF_CldL' Ord_clds']; subst.
  destruct (IHclds _ Ord_p Distinct_Names WF_CldL') as [c_list' [WF_Clds_Constr Sat_Constr']].
  destruct (sat_constr_wf_cld' _ _ Ord_p Distinct_Names WF_cld') as [c_list [WF_cld'_Constr Sat_Constr]].
  exists (c_list ++ c_list'); split.
  constructor; auto.
  apply sat_constr_list_app'; split; auto.
Qed.

Theorem lj_constr_sound : lj_constraint_sound.
  intros; split.
  intros WF_Prog; inversion WF_Prog as [p' p'' H' Distinct_Names WF_Class_List ]; subst; clear WF_Prog.
  generalize (ordered_wf_prog _ _ WF_Class_List) as Ord_p; intros.
  destruct (sat_constr_wf_cld_list' _ _ Ord_p Distinct_Names WF_Class_List) as [c_list [WF_p_Constr Sat_Constr]].
  exists c_list; split; auto.
  constructor; auto.
  intros H; destruct H as [c_list [WF_p_Constr Sat_Constr]].
  inversion WF_p_Constr as [p' c_list' Distinct_Names WF_p_Constr' Ord_p]; subst; eapply wf_program; eauto.
  eapply sat_constr_wf_cld_list; eauto.
Qed.