proposition: Lemma AppL_largest (P: exp X -> Prop) (s: exp X): Dec1 P -> { S & { t | (forall s, s ∈ S -> P s) /\ s = AppL S t /\ forall (u v: exp X), t = u v -> ~ P u}}.
proof: Proof. intros D. induction s. - exists nil. exists (var f). cbn; intuition; discriminate. - exists nil. exists (const c). cbn; intuition; discriminate. - exists nil. exists (lambda s). cbn; intuition; discriminate. - destruct IHs2 as (S & t & ? & -> & ?). destruct (D s1). + exists (s1 :: S). exists t; cbn; intuition; subst; (eauto 2). + exists nil. exists (s1 (AppL S t)). cbn; intuition. injection H1 as ??;subst; intuition. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)