proposition: Lemma retype_Arr n L A: retype_type n (Arr L A) = Arr (retype_ctx n L) (retype_type n A).
proof: Proof. induction L; cbn; eauto; now rewrite IHL. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)