proposition: Lemma type_decompose: forall A, exists L beta, A = Arr L (typevar beta).
proof: Proof. induction A; cbn. - exists nil; exists n. reflexivity. - destruct IHA2 as (L & beta & H). subst. exists (A1 :: L); exists beta. reflexivity. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)