proposition: Lemma abs_subst M (Mabs: isAbs M) G (S: correct_subst M G) (Sabs : isAbs (subst S) := abs_subst_abs Mabs S) (S' : correct_subst (absBody Mabs) (None :: lift_subst G 1) := subst_abs_c Mabs S) : absType Sabs = absType Mabs /\ absBody Sabs = subst S'.
proof: Proof. split. term_inv M. apply abs_type with B. autorewrite with terms; trivial. apply term_eq. assert (absTypeEq: absType Sabs = absType Mabs). term_inv M. apply abs_type with B. rewrite subst_type; trivial. rewrite absBody_env, !subst_env, subst_ran_cons_none, absBody_env. destruct (subst_empty_dec G) as [Ge | Gne]. rewrite subst_ran_lifted_empty; trivial. rewrite subst_ran_empty; simpl; trivial. rewrite !env_sub_Empty, !env_sum_empty_r; trivial. unfold decl; congruence. apply subst_dom_lifted_Empty; trivial. apply subst_dom_Empty; trivial. rewrite subst_ran_lifted_ne; trivial. unfold decl; simpl. rewrite subst_dom_lifted. congruence. term_inv M. rewrite subst_term. assert (Sterm: term (subst S) = \A => presubst_aux Pt 1 (None::G)). rewrite subst_term; trivial. rewrite (absBody_term (subst S) Sabs Sterm). rewrite subst_lift_subst; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)