This is an attribute for simplification rules that are used to normalize casts.

Let r be = or ↔, then elimination lemmas of the shape Π ..., P ↑a1 ... ↑an r P a1 ... an should be given the attribute elim_cast.

This is an attribute for simplification rules that are used to normalize casts.

Let r be = or ↔, then compositional lemmas of the shape Π ..., ↑(P a1 ... an) r P ↑a1 ... ↑an should be given the attribute move_cast.

This is an attribute for simplification rules of the shape Π ..., ↑↑a = ↑a or Π ..., ↑a = a.

They are used in a heuristic to infer intermediate casts.

Normalize casts at the given locations by moving them "upwards". As opposed to simp, norm_cast can be used without necessarily closing the goal.

Rewrite with the given rule and normalize casts between steps.

Normalize the goal and the given expression, then close the goal with exact.

Normalize the goal and the given expression, then apply the expression to the goal.

Normalize the goal and every expression in the local context, then close the goal with assumption.