proposition: Lemma nth_lift_subst_s_rev : forall G i x T, nth_error (lift_subst G i) x = Some (Some T) -> exists T', nth_error G x = Some (Some T') /\ T = lift T' i.
proof: Proof. unfold lift_subst; intros. destruct (nth_map_some_rev G x (fun T => lift_subst_comp T i) H) as [W [GW LW]]. destruct W. exists t; split; try_solve. try_solve. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)