proposition: Lemma Arr_left_injective L1 L2 A: Arr L1 A = Arr L2 A -> L1 = L2.
proof: Proof. destruct (le_ge_dec (length L1) (length L2)); intros H; [|symmetry in H]. all: eapply Arr_inversion in H as [L3]; (eauto 1); intuition. all: destruct L3; simplify in *; (eauto 2). all: eapply (f_equal arity) in H1; cbn in H1; rewrite arity_Arr in H1. all: lia. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)