proposition: Lemma decr_typing L Gamma n sigma: free' (free (length L)) sigma -> L ++ Gamma ⊩(n) sigma : L ++ Gamma -> Gamma ⊩(n) decr (length L) sigma : Gamma.
proof: Proof. intros ? ? x A ?; unfold decr. destruct H as [F1 F2]. eapply ordertyping_weak_preservation_under_renaming with (Gamma := L ++ Gamma). - eapply H0. rewrite nth_error_app2; simplify; eauto. - intros y B H ?. eapply F2 in H2; unfold free in *; eauto. rewrite nth_error_app2 in H; simplify in *; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)