proposition: Lemma nth_lift_normal : forall G i x T, nth_error (lift_subst G i) x = Some (Some T) -> exists2 Tg, T = lift Tg i & nth_error G x = Some (Some Tg).
proof: Proof. induction G; destruct x; try_solve. destruct a; try_solve. exists t; try_solve. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)