proposition: Lemma typing_constEQ x c: x =ₑ 1 ∈ E -> Gamma__dwk ⊢₂(3) constEQ x : alpha → (alpha → alpha) → alpha.
proof: Proof. intros; unfold constEQ. split; cbn [fst snd]. + econstructor; trivial. eapply Gamma__dwk_nth, Vars__de_in; eauto; cbn; intuition. + eapply typing_enc. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)