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