proposition: Lemma terms_conv_shrink_subst : forall M N Q Q', M ~(Q') N -> Q' |=> Q -> (forall x A, activeEnv M |= x := A -> exists y, envSub Q x y) -> M ~(Q) N.
proof: Proof. destruct M as [E Pt T M]; induction M; intros; destruct H. inversion H. destruct (H1 x A). simpl; unfold VarD, decl, EmptyEnv. apply nth_after_copy. replace x1 with y in H7. constructor. simpl; rewrite <- H4; constructor; trivial. apply conv_env_var with x y; auto. apply terms_conv_eq_type; exists Q'; constructor; trivial. apply envSub_Lok with Q' x; trivial. apply H0; trivial. inversion H. constructor. rewrite <- H5; simpl; constructor. intros x y xy A. rewrite activeEnv_funS; simpl; trivial. rewrite activeEnv_funS. split; intro w; destruct x; destruct y; try_solve. apply funS_is_funS with f; auto. inversion H. assert (Nabs: isAbs N). apply abs_isAbs with A R; auto. term_inv N; inversion H6; unfold Tr. assert (MNbody: (buildT M) ~(envSubst_lift1 Q') (buildT T)). constructor. simpl; rewrite <- H10; trivial. change (buildT M) with (absBody (M:=buildT (TAbs M)) I). change (buildT T) with (absBody (M:=buildT (TAbs T)) I). apply conv_env_absBody; trivial. destruct (IHM (buildT T) (envSubst_lift1 Q) (envSubst_lift1 Q')); trivial. apply envSubst_lift1_ext; trivial. fold (activeEnv (buildT M)) in * . intros. destruct x. exists 0; destruct Q; trivial. destruct (H1 x A2). apply varD_tail; trivial. exists (Datatypes.S x0); destruct Q; trivial. constructor; simpl. rewrite H9. constructor; trivial. apply conv_env_abs with I I. simpl; rewrite H9; constructor; trivial. simpl; trivial. inversion H; destruct N as [E' Pt' C N]; destruct N; try discr. apply app_conv with I I. apply IHM1 with Q'; trivial. change (buildT M1) with (appBodyL (M:=buildT (TApp M1 M2)) I). apply app_conv_app_left_aux; constructor; trivial. intros; destruct (H1 x A1). apply (activeEnv_appBodyL_varD (buildT (TApp M1 M2)) I); trivial. exists x0; trivial. apply IHM2 with Q'; trivial. change (buildT M2) with (appBodyR (M:=buildT (TApp M1 M2)) I). apply app_conv_app_right_aux; constructor; trivial. intros; destruct (H1 x A1). apply (activeEnv_appBodyR_varD (buildT (TApp M1 M2)) I); trivial. exists x0; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)