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