proposition: Lemma type_lift Γ t T Γ' : Γ' @ Γ |-- t : T -> forall Γ'', Γ' @ Γ'' @ Γ |-- lift (length Γ') (length Γ'') t : T.
proof: Proof. intros H. depind H; intros; simp lift; eauto with term. generalize (nth_extend_middle unit i Γ0 Γ' Γ''). destruct Nat.compare; intros H'; rewrite H'; simp lift; apply axiom; autorewrite with list in H |- *; lia. apply abstraction. rewrite app_comm_cons. now apply IHtypes. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia