x = h(h(x)+1) is an identity for no h:N→N.
∃x.x≠h(h(x)+1)

Cut-free Positive LCM: each map over N has a minimum point.
∃x.∀y.f(x)≤f(y)

Cut-free Positive LCM: Excluded Middle for 1-quantifiers formulas.
∀x.(∃y.P(x,y)∨∀y.¬P(x,y))

Cut-free Positive LCM: an algorithm learning three x<y<z such that f(x)≤f(y)≤f(z),  interpreted as a proof.
∃x.∃y.( L(x,y) ∧ ∃z. L(y,z) ), with L(x,y) = (x<y∧f(x)≤f(y)).

Cut-free LCM: if x=a satisfies ∀y.P(x,y), then x=a satisfies P(x,b)∧P(x,c).
(∃x.∀y.P(x,y)→∃x.(P(x,b)∧P(x,c)))