proposition: Lemma Arr_inversion L1 L2 A1 A2: length L1 <= length L2 -> Arr L1 A1 = Arr L2 A2 -> exists L, L2 = L1 ++ L /\ A1 = Arr L A2.
proof: Proof. induction L1 in L2, A1, A2 |-*; cbn. - intros _. exists L2. intuition. - destruct L2. inversion 1. intros H H1. cbn in H. eapply le_S_n in H. injection H1 as ??. subst. edestruct IHL1; (eauto 2). intuition. exists x; intuition. f_equal; (eauto 2). Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)