proposition: Lemma Gamma__dwk_nth x: x ∈ Vars__de E -> nth Gamma__dwk x = Some (alpha → (alpha → alpha) → alpha).
proof: Proof. intros H. unfold Gamma__dwk. eapply nth_error_repeated, le_n_S, Sum_in, H. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)