proposition: Lemma beta_subst_stable : forall M N G (MS: correct_subst M G) (NS: correct_subst N G), M -b-> N -> subst MS -b-> subst NS.
proof: Proof. destruct M as [E Pt T M]; induction M; intros. absurd (buildT (TVar v) -b-> N); trivial. apply beta_var_normal; simpl; trivial. absurd (buildT (TFun E f) -b-> N); trivial. apply beta_funS_normal; simpl; trivial. inversion H; try_solve. inversion H0; try_solve. clear Mabs. assert (Mabs: isAbs (buildT (TAbs M))). simpl; trivial. destruct (abs_subst Mabs MS) as [Ms_type Ms_body]. destruct (abs_subst Nabs NS) as [Ns_type Ns_body]. constructor 4 with (abs_subst_abs Mabs MS) (abs_subst_abs Nabs NS). rewrite Ms_type; rewrite Ns_type; trivial. rewrite Ms_body; rewrite Ns_body. apply IHM; trivial. inversion H; try_solve. constructor 1. apply betaStep_subst_stable; trivial. clear Mapp; assert (Mapp: isApp (buildT (TApp M1 M2))); simpl; trivial. destruct (app_subst Mapp MS) as [Ml Mr]. destruct (app_subst Napp NS) as [Nl Nr]. constructor 2 with (app_subst_app Mapp MS) (app_subst_app Napp NS). rewrite Ml; rewrite Nl; apply IHM1; trivial. rewrite Mr; rewrite Nr; trivial. apply term_eq. rewrite !subst_env, <- H1; trivial. rewrite !subst_term, <- H1; trivial. clear Mapp; assert (Mapp: isApp (buildT (TApp M1 M2))); simpl; trivial. destruct (app_subst Mapp MS) as [Ml Mr]. destruct (app_subst Napp NS) as [Nl Nr]. constructor 3 with (app_subst_app Mapp MS) (app_subst_app Napp NS). rewrite Mr; rewrite Nr; apply IHM2; trivial. rewrite Ml; rewrite Nl; trivial. apply term_eq. rewrite !subst_env, <- H1; trivial. rewrite !subst_term, <- H1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)