proposition: Lemma head_decompose s: exists T, s = AppR (head s) T.
proof: Proof. induction s; try solve [exists nil; eauto]. destruct IHs1 as [T]; cbn. exists (s2 :: T); cbn. congruence. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)