proposition: Lemma check_lift_ctx {Γ t T Γ'} : Γ |-- t <= T -> Γ' @ Γ |-- lift 0 (length Γ') t <= T.
proof: Proof. intros. apply (check_lift Γ t T [] H Γ'). Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid