proposition: Lemma nth_lift_subst_sn : forall G i x, nth_error G x = Some None -> nth_error (lift_subst G i) x = Some None.
proof: Proof. unfold lift_subst; intros. rewrite (nth_map_some G x (fun T => lift_subst_comp T i) H). simpl; trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)