proposition: Lemma AppL_decomposition (s: exp X) (n: nat): { '(I, u) | I ⊆ nats n /\ s = AppL (map var I) u /\ forall x v, u = var x v -> ~ x < n }.
proof: Proof. destruct (@AppL_largest _ (fun s => match s with var x => x < n | _ => False end) s) as (S & t & H2 & H3 & H4). intros []; (intuition (auto with typeclass_instances)); now right. subst. induction S. - exists (nil, t). cbn; intuition (auto with listdb). eapply H4; (eauto 2). - edestruct IHS as [[I s'] (H1 & H3 & H5)]. intros; eapply H2; intuition (auto with datatypes). specialize (H2 a); mp H2; destruct a; intuition (auto with datatypes). exists (f :: I, s'); cbn; intuition try congruence. eapply lt_nats in H2. auto with listdb. Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)