proposition: Lemma subst_abs_c M (Mabs: isAbs M) G : correct_subst M G -> correct_subst (absBody Mabs) (None :: lift_subst G 1).
proof: Proof. intro MG. term_inv M. destruct MG. split. intros i j Ti Tj. destruct i; unfold varSubstTo; try_solve. destruct j; try_solve. intros Gi Gj. destruct (nth_lift_normal G 1 i Gi) as [T_i Til Tin]. destruct (nth_lift_normal G 1 j Gj) as [T_j Tjl Tjn]. rewrite Til. rewrite Tjl. rewrite !lift_env. unfold liftedEnv, finalSeg; simpl. rewrite !initialSeg_full; try solve [auto | lia]. apply env_comp_cons; auto. apply (envs_c0 i j); trivial. simpl. unfold decl; apply env_comp_cons; auto. rewrite subst_dom_lifted; trivial. simpl. rewrite subst_ran_cons_none. rewrite subst_dom_lifted. destruct (subst_empty_dec G) as [Ge | Gne]. rewrite subst_ran_lifted_empty; trivial. apply env_comp_sub. apply env_comp_sym. apply env_comp_empty. rewrite subst_ran_lifted_ne; trivial. simpl; unfold decl; apply env_comp_cons; try_solve. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)