proposition: Lemma conv_subst_conv : forall M M' G G' Q (MG: correct_subst M G) (M'G': correct_subst M' G'), M ~(Q) M' -> G ~~(Q) G' -> (subst MG) ~(Q) (subst M'G').
proof: Proof. destruct M as [E Pt T M]; induction M; intros. inversion H; inversion H1. destruct (varSubst_dec G x) as [[T Gx] | Gxn]. destruct (sc_lr H0 y H5 Gx) as [T' [G'y TT']]. assert (MG_term: term (subst MG) = term T). autorewrite with terms using unfold presubst; simpl. rewrite Gx; rewrite lift_0; trivial. assert (M'G'_term: term (subst M'G') = term T'). autorewrite with terms using unfold presubst; rewrite <- H4; simpl. rewrite G'y; rewrite lift_0; trivial. apply terms_conv_diff_env with T'; trivial. apply terms_conv_diff_env_rev with T; trivial. apply equiv_term_activeEnv; trivial. apply subst_env_compat with x; trivial. apply equiv_term_activeEnv; trivial. apply subst_env_compat with y; trivial. term_inv M'. assert (MG_term: term (subst MG) = %x). autorewrite with terms using unfold presubst; simpl. destruct Gxn; rewrite H7; trivial. assert (M'G'_term: term (subst M'G') = %x1). autorewrite with terms using unfold presubst; simpl. inversion H4; rewrite <- H8. destruct (conv_subst_udecl y H0 H5 Gxn); rewrite H7; trivial. apply terms_conv_diff_env with (buildT (TVar T)); trivial. apply terms_conv_diff_env_rev with (buildT (TVar v)); trivial. assert (type (subst MG) = A). autorewrite with terms using trivial. term_inv (subst MG). assert (type (subst M'G') = A0). autorewrite with terms using trivial. term_inv (subst M'G'). inversion H. inversion H1. constructor. rewrite funS_presubst; simpl; trivial. rewrite funS_presubst; trivial. apply funS_is_funS with f; auto. intros x y xy A. rewrite activeEnv_funS. rewrite activeEnv_funS. destruct x; destruct y; try_solve. apply funS_subst_funS. apply funS_is_funS with f; auto. apply funS_is_funS with f. rewrite funS_presubst; simpl; trivial. destruct (abs_subst (M := buildT (TAbs M)) I MG). assert (M'abs: isAbs M'). assert (H': (buildT (TAbs M)) ~ M') by (exists Q; trivial). rewrite <- H'; simpl; trivial. destruct (abs_subst M'abs M'G'). apply abs_conv with (abs_subst_abs (M:=buildT (TAbs M)) I MG) (abs_subst_abs M'abs M'G'); term_inv M'. inversion H; inversion H5; try_solve. rewrite H2; rewrite H4. apply IHM; trivial. constructor; simpl. inversion H; inversion H5; 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. inversion H; inversion H5; trivial. inversion H; trivial. apply subst_conv_cons; trivial. destruct (app_subst (M := buildT (TApp M1 M2)) I MG). assert (M'app: isApp M'). assert (H' : (buildT (TApp M1 M2)) ~ M') by (exists Q; trivial). rewrite <- H'; simpl; trivial. destruct (app_subst M'app M'G'). apply app_conv with (app_subst_app (M:=buildT (TApp M1 M2)) I MG) (app_subst_app M'app M'G'). rewrite H1; rewrite H3. apply IHM1; trivial. change (buildT M1) with (appBodyL (M:=buildT (TApp M1 M2)) I). apply app_conv_app_left_aux; trivial. rewrite H2; rewrite H4. apply IHM2; trivial. change (buildT M2) with (appBodyR (M:=buildT (TApp M1 M2)) I). apply app_conv_app_right_aux; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)