proposition: Lemma firstorder_decidable: Dec1 (OU 1 X).
proof: Proof. intros I. eapply iff_dec. eapply retype_iff; eauto. eapply iff_dec. eapply OU_NOU; eauto. eapply firstorder_decidable'; cbn; eauto 2 using retype_ctx_ord, retype_type_ord, eta₀_normal. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)