proposition: Lemma decomp'_typing Gamma E E': decomp' E = Some E' -> forall L, all_terms (@lambda_free X) E -> Gamma ⊢₊₊(1) E : L -> exists L, Gamma ⊢₊₊(1) E' : L.
proof: Proof. decomp_ind; eauto. intros s t E E1 E2 H H' IH L LF T. inv T. simplify in LF; intuition idtac. eapply decomp_typing in H as [L1]; eauto. edestruct IH as [L2]; eauto. exists (L1 ++ L2). eapply ordertyping_combine; unfold left_side, right_side; simplify. 1 - 2: eapply orderlisttyping_app; try eapply left_ordertyping; try eapply right_ordertyping. all: eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)