proposition: Lemma synth_liftn {Γ Γ' 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 Arith Wf_nat