proposition: Lemma check_lift_gen Δ t T (H : Δ |-- t <= T) : forall Γ Γ', Δ = Γ' @ Γ -> forall Γ'', Γ' @ Γ'' @ Γ |-- lift (length Γ') (length Γ'') t <= T with synthetize_lift_gen Δ t T (H : Δ |-- t => T) : forall Γ Γ', Δ = Γ' @ Γ -> forall Γ'', Γ' @ Γ'' @ Γ |-- lift (length Γ') (length Γ'') t => T.
proof: Proof. destruct H; intros; simp lift. econstructor. change (S (length Γ')) with (length (A :: Γ')). change (A :: Γ' @ Γ'' @ Γ0) with ((A :: Γ') @ Γ'' @ Γ0). eapply check_lift_gen; try eassumption. subst. rewrite app_comm_cons; subst; try eassumption; trivial. econstructor; eapply check_lift_gen; eassumption. econstructor. econstructor. eassumption. eapply synthetize_lift_gen; eassumption. destruct H; intros; simp lift; try solve [econstructor; term]. clear check_lift_gen synthetize_lift_gen. subst. generalize (nth_extend_middle unit i Γ0 Γ' Γ''). destruct Nat.compare; intros H'; rewrite H'; simp lift; apply axiom_synth; autorewrite with list in H |- *; lia. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid