proposition: Lemma horpo_var_consistent_aux : forall M N, (forall M' N', (subterm M' M \/ (M' = M /\ subterm N' N)) -> M' >> N' -> envSubset (activeEnv N') (activeEnv M')) -> M >> N -> envSubset (activeEnv N) (activeEnv M).
proof: Proof. intros M N IH MN. destruct MN as [M N MNtype MNenv Mnorm Nnorm M_N]. destruct M_N as [ M N MFapp Cond | M N f g Mf Ng f_g M_Nargs | M N f Mf Nf MNargs | M N Ns Mfapp NsN MNs | M N Mapp Napp Mnfapp _ LL | M N Mabs Nabs MN | M N MNbeta]. destruct Cond as [Msub Msub_arg Cond]. destruct Cond. apply env_subset_trans with (activeEnv M0). apply IH; trivial. left; apply arg_subterm; trivial. apply activeEnv_subset_arg; trivial. apply activeEnv_subset_arg; trivial. apply activeEnv_subset_units; intros. destruct (appUnit_head_or_arg N N' H). rewrite (activeEnv_funS). apply env_subset_empty. apply funS_is_funS with g; rewrite H0; trivial. apply horpo_args_var_consistent with (appArgs N); trivial. intros. apply IH; trivial. destruct H1; auto. right; destruct H1; split; trivial. apply arg_subterm; trivial. apply activeEnv_subset_units; intros. destruct (appUnit_head_or_arg N N' H). rewrite (activeEnv_funS). apply env_subset_empty. apply funS_is_funS with f; rewrite H0; trivial. inversion MNargs. set (N'mul := member_list_multiset (appArgs N) N' H0). destruct (mOrd_elts_ge H1 N'mul). destruct H5. apply env_subset_trans with (activeEnv x). apply IH; trivial. destruct (member_multiset_list (appArgs M) H4). left; apply arg_subterm. unfold eqA in H7; unfold TermsEqset.eqA in H7; rewrite H7; trivial. apply activeEnv_subset_arg. destruct (member_multiset_list (appArgs M) H4). inversion H7; apply H6. inversion H5; rewrite <- H6. apply activeEnv_subset_arg. destruct (member_multiset_list (appArgs M) H4). inversion H8; apply H7. apply activeEnv_subset_partialFlattening with Ns; trivial; intros. apply horpo_args_var_consistent with Ns; trivial. intros. apply IH; trivial. destruct H0; auto. right; destruct H0; split; trivial. apply partialFlattening_subterm with Ns; trivial. rewrite (activeEnv_app M Mapp), (activeEnv_app N Napp). destruct (horpo_app M N Mapp Napp MNtype LL) as [L_L [R_R str]]. apply env_subset_sum. apply activeEnv_app_comp. inversion L_L. apply IH; trivial. left; apply appBodyL_subterm. rewrite H1; apply env_subset_refl. inversion R_R. apply IH; trivial. left; apply appBodyR_subterm. rewrite H1; apply env_subset_refl. rewrite activeEnv_abs with M Mabs, activeEnv_abs with N Nabs. apply env_subset_tail. apply IH; trivial. left; apply absBody_subterm. apply beta_var_consistent. hyp. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)