fact: Definition check_lift Γ t T Γ' (H : Γ' @ Γ |-- t <= T) : forall Γ'', Γ' @ Γ'' @ Γ |-- lift (length Γ') (length Γ'') t <= T := check_lift_gen (Γ' @ Γ) _ _ H _ _ eq_refl.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid