Using local notation inside a Coq theorem

Question

Suppose I want to prove a theorem about an object that is verbose to spell out, say ABCDEFGHIJKLMNOPQRSTUVWXYZ, such that the unabbreviated theorem is

Theorem verbose :
prop_1 ABCDEFGHIJKLMNOPQRSTUVWXYZ
-> prop_2 ABCDEFGHIJKLMNOPQRSTUVWXYZ
-> prop_3 ABCDEFGHIJKLMNOPQRSTUVWXYZ
-> prop_4 ABCDEFGHIJKLMNOPQRSTUVWXYZ
-> prop_5 ABCDEFGHIJKLMNOPQRSTUVWXYZ.

Is there a way to use local notation inside a theorem, so I can compress it to something like the following?

Theorem succinct :
prop_1 X -> prop_2 X -> prop_3 X -> prop_4 X -> prop_5 X
where "X" := ABCDEFGHIJKLMNOPQRSTUVWXYZ.

I'd use regular notations if I'm using the verbose term repeatedly, but for one-off cases it'd be nice if there were something like where for theorems, so I can reuse good names.

Answer 1

You can use Sections and Let for local definitions.

Section thm.

Let X := ABCDEFGHIJKLMNOPQRSTUVWXYZ.

Theorem succinct : prop_1 X -> prop_2 X.

....

End thm.

Answer 2

You can use Definition myobj := ABCDEFGHIJKLMNOPQRSTUVWXYZ. to define a name for the object. Later, you can use unfold myobj. to expand the name to its value.

To introduce it into a local proof environment, use remember.

Theorem foo:
    forall x y z : Z, x + y - z = x + (y - z).
    intros.
    remember (x+y) as bar.

Now the environment is

...
Heqbar : bar = x + y
============================
bar - z = x + (y - z)