proposition: Lemma normal_retyping n Gamma (s: exp X) A: normal s -> Gamma ⊢(n) s : A -> retype_ctx n Gamma ⊢(n) s : retype_type n A.
proof: Proof. intros H % normal_nf; induction H in Gamma, A |-*; subst. intros (L & B & ? & -> & ?) % Lambda_ordertyping_inv. rewrite retype_Arr. eapply Lambda_ordertyping; [unfold retype_ctx; now simplify|]. unfold retype_ctx; rewrite <-map_rev, <-map_app; fold (retype_ctx n (rev L ++ Gamma)). eapply AppR_ordertyping_inv in H0 as (L' & ? & ?). assert (ord' L' <= n). - destruct s; destruct i; inv H2; simplify in H4. now intuition auto. rewrite H4 in H5; simplify in H5; intuition (auto with arith). - eapply AppR_ordertyping with (L := retype_ctx n L'). + clear H2. induction H0; eauto. econstructor. all: cbn in H3; simplify in H3. 2:intuition (auto with datatypes). destruct dec2; intuition trivial. erewrite <-retype_type_id; [| transitivity n; eauto]. eapply H; cbn; auto. + unfold retype_ctx at 2; rewrite <-map_rev; fold (retype_ctx n (rev L')). rewrite <-retype_Arr. destruct s; destruct i. all: inv H2; rewrite retype_type_id. 2-4:eauto. econstructor; eauto. unfold retype_ctx; erewrite map_nth_error; eauto. destruct dec2; easy. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)