proposition: Lemma ordertyping_from_basetyping Sigma u B: (forall c, c ∈ consts u -> ord (ctype X c) <= S n) -> Sigma ⊢ u : B -> normal u -> ord B <= S n -> ord' Sigma <= n -> Sigma ⊢(n) u : B.
proof: Proof. induction 2; [eauto|eauto| |]. - simplify; intros; econstructor; eapply IHtyping; intuition trivial. eauto using normal_lam_elim. cbn; simplify; intuition (auto with arith). - intros; enough (ord A <= n). + econstructor; [eapply IHtyping1 | eapply IHtyping2]. 1, 5: intros; eapply H; cbn; intuition (auto with datatypes). 1, 4: eauto using normal_app_r, normal_app_l. 2, 4: eauto. 1, 2: simplify; eauto; intuition (auto with arith). + eapply head_atom in H0; [|easy]. cbn in H0. destruct (head_decompose s) as [T]. rewrite H3 in H0_. eapply AppR_typing_inv in H0_ as (? & ? & ?). enough (ord (Arr (rev x) (A → B)) <= S n) as H6 by (simplify in H6; intuition (auto with arith)). destruct (head s); cbn in H0; eauto. all: inv H5. eapply ord'_elements in H2; eauto. eapply H; cbn; simplify; cbn; intuition trivial. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)