proposition: Lemma decomp_typing s t E Gamma: decomp s t = Some E -> forall A, lambda_free s -> lambda_free t -> (Gamma ⊢(1) s : A) -> (Gamma ⊢(1) t : A) -> exists L, Gamma ⊢₊₊(1) E : L.
proof: Proof. decomp_ind; intros. - exists nil; econstructor. - exists [A]; eauto using eqs_ordertyping. - exists [A]; eauto using eqs_ordertyping. - inv H4. inv H5. inv H6. inv H7. enough (A0 → A = A1 → A) as H4. injection H4 as ->. edestruct H1 as [L1]; eauto. edestruct H3 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; eauto. eapply lambda_free_normal in H10 as H10'; eapply lambda_free_not_lam in H10 as H10''. eapply lambda_free_normal in H9 as H9'; eapply lambda_free_not_lam in H9 as H9''. eapply head_atom in H10' as H10'''; eauto. eapply head_atom in H9' as H9'''; eauto. destruct (head_decompose s1) as [S1]. destruct (head_decompose t1) as [T1]. destruct (head s1); cbn in *;[ | | easy..];[| destruct (head t1)]; cbn in *. 4,5: easy. 1: subst s1; eapply AppR_ordertyping_inv in H8 as (L & ? & V); inv V. 2: subst t1; eapply AppR_ordertyping_inv in H6 as (L & ? & V); inv V. 1: rewrite ord_Arr in H8; eapply Nat.max_lub_r, ord_arr_one in H8 as []. 1: rewrite ord_Arr in H7; eapply Nat.max_lub_r, ord_arr_one in H7 as []. eapply decomp_some_head_consts in H0; subst; simplify; cbn; eauto. subst. eapply AppR_ordertyping_inv in H8 as (L1 & ? & ?). eapply AppR_ordertyping_inv in H6 as (L2 & ? & ?). inv H4. inv H6. rewrite H7 in H8. change (A0 → A) with (Arr [A0] A) in H8. change (A1 → A) with (Arr [A1] A) in H8. rewrite <-!Arr_app in H8. eapply Arr_left_injective in H8. eapply app_injective_right in H8. 2: easy. intuition congruence. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)