proposition: Lemma lifted_subst_envs_comp G n : subst_envs_comp G -> subst_envs_comp (lift_subst G n).
proof: Proof. unfold subst_envs_comp. intros G_comp i j Ti Tj Gi Gj p. destruct (nth_lift_normal G n i Gi) as [T_i TiL TiG]. destruct (nth_lift_normal G n j Gj) as [T_j TjL TjG]. rewrite TiL. rewrite TjL. do 2 rewrite lift_env. unfold liftedEnv, env_comp_on, VarD; simpl. case (le_lt_dec n p). intro n_le_p. rewrite !nth_app_right; autorewrite with datatypes using trivial. unfold finalSeg; simpl. repeat rewrite initialSeg_full; try solve [auto with datatypes | lia]. exact (G_comp i j T_i T_j TiG TjG (p-n)). intro p_lt_n. rewrite !nth_app_left; autorewrite with datatypes using try_solve. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)