MATH.12:4.3 - Compose the operations and simplify their use

Substitute each supplied result into the place that consumes it. Preserve names for inputs whose values differ or whose dependencies matter.

Some simplifications directly expose a wanted value:

• Applying x ↦ t(x) to a gives t with a substituted for x.
• The first component of (b,c) is b; the second is c.
• A case distinction applied to a tagged value runs the branch named by its tag.

These are computation rules for the chosen constructions. Use their conditions, including the input type and any variable binding. Rename an auxiliary variable when substitution would confuse it with another input.

For a proof supplying a dependent pair p(x)=(y,q), define F(x) as its first component. The second component then supplies R(x,F(x)). This gives both an obtaining operation and the relation its output satisfies, provided the construction of p(x) is available.

Write the resulting expression or procedure in a representation the receiver can use. A short formula can be sufficient. Pseudocode or a proof-assistant term is useful when its evaluation or composition is the next question.