Term rewriting and simplification¶
Rewriting expressions¶
These tactics use the equality eq:forall A:Type, A>A>Prop
defined in
file Logic.v
(see Logic). The notation for eq T t u
is
simply t=u
dropping the implicit type of t
and u
.

Tactic
rewrite term
¶ This tactic applies to any goal. The type of
term
must have the formforall (x
_{1}:A
_{1}) ... (x
_{n}:A
_{n}), eq term
_{1}term
_{2}.
where
eq
is the Leibniz equality or a registered setoid equality.Then
rewrite term
finds the first subterm matchingterm
_{1} in the goal, resulting in instancesterm
_{1}' andterm
_{2}' and then replaces every occurrence ofterm
_{1}' byterm
_{2}'. Hence, some of the variablesx
_{i} are solved by unification, and some of the typesA
_{1}, ..., A
_{n} become new subgoals.
Error
Tactic generated a subgoal identical to the original goal. This happens if term does not occur in the goal.
¶

Variant
rewrite term in goal_occurrences
Analogous to
rewrite term
but rewriting is done following the clausegoal_occurrences
. For instance:rewrite H in H'
will rewriteH
in the hypothesisH'
instead of the current goal.rewrite H in H' at 1, H'' at  2  *
meansrewrite H; rewrite H in H' at 1; rewrite H in H'' at  2.
In particular a failure will happen if any of these three simpler tactics fails.rewrite H in * 
will dorewrite H in H'
for all hypothesesH'
different fromH
. A success will happen as soon as at least one of these simpler tactics succeeds.rewrite H in *
is a combination ofrewrite H
andrewrite H in * 
that succeeds if at least one of these two tactics succeeds.
Orientation
>
or<
can be inserted before theterm
to rewrite.

Variant
rewrite term at occurrences
Rewrite only the given
occurrences
ofterm
. Occurrences are specified from left to right as for pattern (pattern
). The rewrite is always performed using setoid rewriting, even for Leibniz’s equality, so one has toImport Setoid
to use this variant.

Variant
rewrite term by tactic
Use tactic to completely solve the sideconditions arising from the
rewrite
.

Variant
rewrite orientation term+, in ident?
Is equivalent to the
n
successive tacticsrewrite term+;
, each one working on the first subgoal generated by the previous one. Anorientation
>
or<
can be inserted before eachterm
to rewrite. One unique clause can be added at the end after the keyword in; it will then affect all rewrite operations.
In all forms of rewrite described above, a
term
to rewrite can be immediately prefixed by one of the following modifiers:?
: the tacticrewrite ?term
performs the rewrite ofterm
as many times as possible (perhaps zero time). This form never fails.natural?
: works similarly, except that it will do at mostnatural
rewrites.!
: works as?
, except that at least one rewrite should succeed, otherwise the tactic fails.natural!
(or simplynatural
) : preciselynatural
rewrites ofterm
will be done, leading to failure if thesenatural
rewrites are not possible.

Variant
erewrite term
¶ This tactic works as
rewrite term
but turning unresolved bindings into existential variables, if any, instead of failing. It has the same variants asrewrite
has.

Flag
Keyed Unification
¶ Makes higherorder unification used by
rewrite
rely on a set of keys to drive unification. The subterms, considered as rewriting candidates, must start with the same key as the left or righthand side of the lemma given to rewrite, and the arguments are then unified up to full reduction.

Error

Tactic
replace term with term’
¶ This tactic applies to any goal. It replaces all free occurrences of
term
in the current goal withterm’
and generates an equalityterm = term’
as a subgoal. This equality is automatically solved if it occurs among the assumptions, or if its symmetric form occurs. It is equivalent tocut term = term’; [intro H
_{n}; rewrite < H
_{n}; clear H
_{n} assumption  symmetry; try assumption]
.
Error
Terms do not have convertible types.
¶

Variant
replace term with term’ by tactic
This acts as
replace term with term’
but appliestactic
to solve the generated subgoalterm = term’
.

Variant
replace term
Replaces
term
withterm’
using the first assumption whose type has the formterm = term’
orterm’ = term
.

Variant
replace > term
Replaces
term
withterm’
using the first assumption whose type has the formterm = term’

Variant
replace < term
Replaces
term
withterm’
using the first assumption whose type has the formterm’ = term

Variant
replace term with term? in goal_occurrences by tactic?

Variant
replace > term in goal_occurrences

Variant
replace < term in goal_occurrences
Acts as before but the replacements take place in the specified clauses (
goal_occurrences
) (see Performing computations) and not only in the conclusion of the goal. The clause argument must not contain anytype of
norvalue of
.

Error

Tactic
subst ident
¶ This tactic applies to a goal that has
ident
in its context and (at least) one hypothesis, sayH
, of typeident = t
ort = ident
withident
not occurring int
. Then it replacesident
byt
everywhere in the goal (in the hypotheses and in the conclusion) and clearsident
andH
from the context.If
ident
is a local definition of the formident := t
, it is also unfolded and cleared.If
ident
is a section variable it is expected to have no indirect occurrences in the goal, i.e. that no global declarations implicitly depending on the section variable must be present in the goal.Note

Variant
subst
This applies
subst
repeatedly from top to bottom to all hypotheses of the context for which an equality of the formident = t
ort = ident
orident := t
exists, withident
not occurring int
andident
not a section variable with indirect dependencies in the goal.

Flag
Regular Subst Tactic
¶ This flag controls the behavior of
subst
. When it is activated (it is by default),subst
also deals with the following corner cases:A context with ordered hypotheses
ident
_{1}= ident
_{2} andident
_{1}= t
, ort′ = ident
_{1`} witht′
not a variable, and no other hypotheses of the formident
_{2}= u
oru = ident
_{2}; without the flag, a second call to subst would be necessary to replaceident
_{2} byt
ort′
respectively.The presence of a recursive equation which without the flag would be a cause of failure of
subst
.A context with cyclic dependencies as with hypotheses
ident
_{1}= f ident
_{2} andident
_{2}= g ident
_{1} which without the flag would be a cause of failure ofsubst
.
Additionally, it prevents a local definition such as
ident := t
to be unfolded which otherwise it would exceptionally unfold in configurations containing hypotheses of the formident = u
, oru′ = ident
withu′
not a variable. Finally, it preserves the initial order of hypotheses, which without the flag it may break. default.

Error
Section variable :n:`ident` occurs implicitly in global declaration :n:`qualid` present in hypothesis :n:`ident`.
¶ 
Error
Section variable :n:`ident` occurs implicitly in global declaration :n:`qualid` present in the conclusion.
¶ Raised when the variable is a section variable with indirect dependencies in the goal.

Variant

Tactic
stepl term
¶ This tactic is for chaining rewriting steps. It assumes a goal of the form
R term term
whereR
is a binary relation and relies on a database of lemmas of the formforall x y z, R x y > eq x z > R z y
whereeq
is typically a setoid equality. The application ofstepl term
then replaces the goal byR term term
and adds a new goal statingeq term term
.This tactic is especially useful for parametric setoids which are not accepted as regular setoids for
rewrite
andsetoid_replace
(see Generalized rewriting).

Tactic
change term
¶ This tactic applies to any goal. It implements the rule
Conv
given in Subtyping rules.change U
replaces the current goalT
withU
providing thatU
is wellformed and thatT
andU
are convertible.
Error
Not convertible.
¶

Variant
change term with term’
This replaces the occurrences of
term
byterm’
in the current goal. The termterm
andterm’
must be convertible.

Variant
change term at natural+ with term’
This replaces the occurrences numbered
natural+
ofterm
byterm’
in the current goal. The termsterm
andterm’
must be convertible.
Error
Too few occurrences.
¶

Error

Variant
change term at natural+? with term? in goal_occurrences
In the presence of
with
, this applieschange
to the occurrences specified bygoal_occurrences
. In the absence ofwith
,goal_occurrences
is expected to only list hypotheses (and optionally the conclusion) without specifying occurrences (i.e. noat
clause).

Variant
now_show term
This is a synonym of
change term
. It can be used to make some proof steps explicit when refactoring a proof script to make it readable.
See also

Error
Performing computations¶
This set of tactics implements different specialized usages of the
tactic change
.
All conversion tactics (including change
) can be parameterized by the
parts of the goal where the conversion can occur. This is done using
goal clauses which consists in a list of hypotheses and, optionally,
of a reference to the conclusion of the goal. For defined hypothesis
it is possible to specify if the conversion should occur on the type
part, the body part or both (default).
Goal clauses are written after a conversion tactic (tactics set
,
rewrite
, replace
and autorewrite
also use goal
clauses) and are introduced by the keyword in
. If no goal clause is
provided, the default is to perform the conversion only in the
conclusion.
For backward compatibility, the notation in ident+
performs
the conversion in hypotheses ident+
.

Tactic
cbv strategy_flag?
¶ 
Tactic
lazy strategy_flag?
¶ These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. In correspondence with the kinds of reduction considered in Coq namely \(\beta\) (reduction of functional application), \(\delta\) (unfolding of transparent constants, see Controlling the reduction strategies and the conversion algorithm), \(\iota\) (reduction of pattern matching over a constructed term, and unfolding of
fix
andcofix
expressions) and \(\zeta\) (contraction of local definitions), the flags are eitherbeta
,delta
,match
,fix
,cofix
,iota
orzeta
. Theiota
flag is a shorthand formatch
,fix
andcofix
. Thedelta
flag itself can be refined intodelta [ qualid+ ]
ordelta  [ qualid+ ]
, restricting in the first case the constants to unfold to the constants listed, and restricting in the second case the constant to unfold to all but the ones explicitly mentioned. Notice that thedelta
flag does not apply to variables bound by a letin construction inside theterm
itself (use here thezeta
flag). In any cases, opaque constants are not unfolded (see Controlling the reduction strategies and the conversion algorithm).Normalization according to the flags is done by first evaluating the head of the expression into a weakhead normal form, i.e. until the evaluation is blocked by a variable (or an opaque constant, or an axiom), as e.g. in
x u1 ... un
, ormatch x with ... end
, or(fix f x {struct x} := ...) x
, or is a constructed form (a \(\lambda\)expression, a constructor, a cofixpoint, an inductive type, a product type, a sort), or is a redex that the flags prevent to reduce. Once a weakhead normal form is obtained, subterms are recursively reduced using the same strategy.Reduction to weakhead normal form can be done using two strategies: lazy (
lazy
tactic), or callbyvalue (cbv
tactic). The lazy strategy is a callbyneed strategy, with sharing of reductions: the arguments of a function call are weakly evaluated only when necessary, and if an argument is used several times then it is weakly computed only once. This reduction is efficient for reducing expressions with dead code. For instance, the proofs of a propositionexists x. P(x)
reduce to a pair of a witnesst
, and a proof thatt
satisfies the predicateP
. Most of the time,t
may be computed without computing the proof ofP(t)
, thanks to the lazy strategy.The callbyvalue strategy is the one used in ML languages: the arguments of a function call are systematically weakly evaluated first. Despite the lazy strategy always performs fewer reductions than the callbyvalue strategy, the latter is generally more efficient for evaluating purely computational expressions (i.e. with little dead code).

Variant
lazy
This is a synonym for
lazy beta delta iota zeta
.

Variant
compute [ qualid+ ]

Variant
cbv [ qualid+ ]
These are synonyms of
cbv beta delta qualid+ iota zeta
.

Variant
compute  [ qualid+ ]

Variant
cbv  [ qualid+ ]
These are synonyms of
cbv beta delta qualid+ iota zeta
.

Variant
lazy [ qualid+ ]

Variant
lazy  [ qualid+ ]
These are respectively synonyms of
lazy beta delta qualid+ iota zeta
andlazy beta delta qualid+ iota zeta
.

Variant
vm_compute
¶ This tactic evaluates the goal using the optimized callbyvalue evaluation bytecodebased virtual machine described in [GregoireL02]. This algorithm is dramatically more efficient than the algorithm used for the
cbv
tactic, but it cannot be finetuned. It is especially interesting for full evaluation of algebraic objects. This includes the case of reflectionbased tactics.

Variant
native_compute
¶ This tactic evaluates the goal by compilation to OCaml as described in [BDenesGregoire11]. If Coq is running in native code, it can be typically two to five times faster than
vm_compute
. Note however that the compilation cost is higher, so it is worth using only for intensive computations.
Flag
NativeCompute Timing
¶ This flag causes all calls to the native compiler to print timing information for the conversion to native code, compilation, execution, and reification phases of native compilation. Timing is printed in units of seconds of wallclock time.

Flag
NativeCompute Profiling
¶ On Linux, if you have the
perf
profiler installed, this flag makes it possible to profilenative_compute
evaluations.

Option
NativeCompute Profile Filename string
¶ This option specifies the profile output; the default is
native_compute_profile.data
. The actual filename used will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. That means you can individually profile multiple uses ofnative_compute
in a script. From the Linux command line, runperf report
on the profile file to see the results. Consult theperf
documentation for more details.

Flag

Flag
Debug Cbv
¶ This flag makes
cbv
(and its derivativecompute
) print information about the constants it encounters and the unfolding decisions it makes.

Tactic
red
¶ This tactic applies to a goal that has the form:
forall (x:T1) ... (xk:Tk), T
with
T
\(\beta\)\(\iota\)\(\zeta\)reducing toc t
_{1}... t
_{n} andc
a constant. Ifc
is transparent then it replacesc
with its definition (sayt
) and then reduces(t t
_{1}... t
_{n})
according to \(\beta\)\(\iota\)\(\zeta\)reduction rules.

Error
Not reducible.
¶

Error
No head constant to reduce.
¶

Tactic
hnf
¶ This tactic applies to any goal. It replaces the current goal with its head normal form according to the \(\beta\)\(\delta\)\(\iota\)\(\zeta\)reduction rules, i.e. it reduces the head of the goal until it becomes a product or an irreducible term. All inner \(\beta\)\(\iota\)redexes are also reduced. The behavior of both
hnf
can be tuned using theArguments
command.Example: The term
fun n : nat => S n + S n
is not reduced byhnf
.
Note
The \(\delta\) rule only applies to transparent constants (see Controlling the reduction strategies and the conversion algorithm on transparency and opacity).

Tactic
cbn
¶ 
Tactic
simpl
¶ These tactics apply to any goal. They try to reduce a term to something still readable instead of fully normalizing it. They perform a sort of strong normalization with two key differences:
They unfold a constant if and only if it leads to a \(\iota\)reduction, i.e. reducing a match or unfolding a fixpoint.
While reducing a constant unfolding to (co)fixpoints, the tactics use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls.
The
cbn
tactic is claimed to be a more principled, faster and more predictable replacement forsimpl
.The
cbn
tactic accepts the same flags ascbv
andlazy
. The behavior of bothsimpl
andcbn
can be tuned using theArguments
command.Notice that only transparent constants whose name can be reused in the recursive calls are possibly unfolded by
simpl
. For instance a constant defined byplus' := plus
is possibly unfolded and reused in the recursive calls, but a constant such assucc := plus (S O)
is never unfolded. This is the main difference betweensimpl
andcbn
. The tacticcbn
reduces whenever it will be able to reuse it or not:succ t
is reduced toS t
.

Variant
cbn [ qualid+ ]

Variant
cbn  [ qualid+ ]
These are respectively synonyms of
cbn beta delta [ qualid+ ] iota zeta
andcbn beta delta  [ qualid+ ] iota zeta
(seecbn
).

Variant
simpl pattern at natural+
This applies
simpl
only to thenatural+
occurrences of the subterms matchingpattern
in the current goal.
Error
Too few occurrences.
¶

Error

Variant
simpl qualid

Variant
simpl string
This applies
simpl
only to the applicative subterms whose head occurrence is the unfoldable constantqualid
(the constant can be referred to by its notation usingstring
if such a notation exists).

Variant
simpl qualid at natural+

Variant
simpl string at natural+
This applies
simpl
only to thenatural+
applicative subterms whose head occurrence isqualid
(orstring
).

Flag
Debug RAKAM
¶ This flag makes
cbn
print various debugging information.RAKAM
is the Refolding Algebraic Krivine Abstract Machine.

Tactic
unfold qualid
¶ This tactic applies to any goal. The argument qualid must denote a defined transparent constant or local definition (see Toplevel definitions and Controlling the reduction strategies and the conversion algorithm). The tactic
unfold
applies the \(\delta\) rule to each occurrence of the constant to whichqualid
refers in the current goal and then replaces it with its \(\beta\iota\zeta\)normal form. Use the general reduction tactics if you want to avoid this final reduction, for instancecbv delta [qualid]
.
Error
Cannot coerce qualid to an evaluable reference.
¶ This error is frequent when trying to unfold something that has defined as an inductive type (or constructor) and not as a definition.
Example
 Goal 0 <= 1.
 1 subgoal ============================ 0 <= 1
 unfold le.
 Toplevel input, characters 79: > unfold le. > ^^ Error: Cannot turn inductive le into an evaluable reference.
This error can also be raised if you are trying to unfold something that has been marked as opaque.
Example
 Opaque Nat.add.
 Goal 1 + 0 = 1.
 1 subgoal ============================ 1 + 0 = 1
 unfold Nat.add.
 Toplevel input, characters 014: > unfold Nat.add. > ^^^^^^^^^^^^^^ Error: Nat.add is opaque.

Variant
unfold qualid in goal_occurrences
Replaces
qualid
in hypothesis (or hypotheses) designated bygoal_occurrences
with its definition and replaces the hypothesis with its \(\beta\)\(\iota\) normal form.

Variant
unfold qualid+,
Replaces
qualid+,
with their definitions and replaces the current goal with its \(\beta\)\(\iota\) normal form.

Variant
unfold qualid at occurrences+,
The list
occurrences
specify the occurrences ofqualid
to be unfolded. Occurrences are located from left to right.

Variant
unfold string
If
string
denotes the discriminating symbol of a notation (e.g. "+") or an expression defining a notation (e.g."_ + _"
), and this notation denotes an application whose head symbol is an unfoldable constant, then the tactic unfolds it.

Variant
unfold string%ident
This is variant of
unfold string
wherestring
gets its interpretation from the scope bound to the delimiting keyident
instead of its default interpretation (see Local interpretation rules for notations).

Variant
unfold qualidstring%ident? at occurrences?+, in goal_occurrences?
This is the most general form.

Error

Tactic
fold term
¶ This tactic applies to any goal. The term
term
is reduced using thered
tactic. Every occurrence of the resultingterm
in the goal is then replaced byterm
. This tactic is particularly useful when a fixpoint definition has been wrongfully unfolded, making the goal very hard to read. On the other hand, when an unfolded function applied to its argument has been reduced, thefold
tactic won't do anything.Example
 Goal ~0=0.
 1 subgoal ============================ 0 <> 0
 unfold not.
 1 subgoal ============================ 0 = 0 > False
 Fail progress fold not.
 The command has indeed failed with message: Failed to progress.
 pattern (0 = 0).
 1 subgoal ============================ (fun P : Prop => P > False) (0 = 0)
 fold not.
 1 subgoal ============================ 0 <> 0

Tactic
pattern term
¶ This command applies to any goal. The argument
term
must be a free subterm of the current goal. The command pattern performs \(\beta\)expansion (the inverse of \(\beta\)reduction) of the current goal (sayT
) byreplacing all occurrences of
term
inT
with a fresh variableabstracting this variable
applying the abstracted goal to
term
For instance, if the current goal
T
is expressible as \(\varphi\)(t)
where the notation captures all the instances oft
in \(\varphi\)(t)
, thenpattern t
transforms it into(fun x:A =>
\(\varphi\)(x)) t
. This tactic can be used, for instance, when the tacticapply
fails on matching.

Variant
pattern term at natural+
Only the occurrences
natural+
ofterm
are considered for \(\beta\)expansion. Occurrences are located from left to right.

Variant
pattern term at  natural+
All occurrences except the occurrences of indexes
natural+
ofterm
are considered for \(\beta\)expansion. Occurrences are located from left to right.

Variant
pattern term+,
Starting from a goal \(\varphi\)
(t
_{1}... t
_{m})
, the tacticpattern t
_{1}, ..., t
_{m} generates the equivalent goal(fun (x
_{1}:A
_{1}) ... (x
_{m}:A
_{m}) =>
\(\varphi\)(x
_{1}... x
_{m})) t
_{1}... t
_{m}. Ift
_{i} occurs in one of the generated typesA
_{j} these occurrences will also be considered and possibly abstracted.

Variant
pattern term at natural++,
This behaves as above but processing only the occurrences
natural+
ofterm
starting fromterm
.

Variant
pattern term at ? natural+,?+,
This is the most general syntax that combines the different variants.

Tactic
with_strategy strategy_level_or_var [ reference+ ] ltac_expr3
¶ Executes
ltac_expr3
, applying the alternate unfolding behavior that theStrategy
command controls, but only forltac_expr3
. This can be useful for guarding calls to reduction in tactic automation to ensure that certain constants are never unfolded by tactics likesimpl
andcbn
or to ensure that unfolding does not fail.Example
 Opaque id.
 Goal id 10 = 10.
 1 subgoal ============================ id 10 = 10
 Fail unfold id.
 The command has indeed failed with message: id is opaque.
 with_strategy transparent [id] unfold id.
 1 subgoal ============================ 10 = 10
Warning
Use this tactic with care, as effects do not persist past the end of the proof script. Notably, this finetuning of the conversion strategy is not in effect during
Qed
norDefined
, so this tactic is most useful either in combination withabstract
, which will check the proof early while the finetuning is still in effect, or to guard calls to conversion in tactic automation to ensure that, e.g.,unfold
does not fail just because the user made a constantOpaque
.This can be illustrated with the following example involving the factorial function.
 Fixpoint fact (n : nat) : nat := match n with  0 => 1  S n' => n * fact n' end.
 fact is defined fact is recursively defined (guarded on 1st argument)
Suppose now that, for whatever reason, we want in general to unfold the
id
function very late during conversion: Strategy 1000 [id].
If we try to prove
id (fact n) = fact n
byreflexivity
, it will now take time proportional to \(n!\), because Coq will keep unfoldingfact
and*
and+
before it unfoldsid
, resulting in a full computation offact n
(in unary, because we are usingnat
), which takes time \(n!\). We can see this cross the relevant threshold at around \(n = 9\): Goal True.
 1 subgoal ============================ True
 Time assert (id (fact 8) = fact 8) by reflexivity.
 Finished transaction in 0.384 secs (0.172u,0.212s) (successful) 1 subgoal H : id (fact 8) = fact 8 ============================ True
 Time assert (id (fact 9) = fact 9) by reflexivity.
 Finished transaction in 1.391 secs (1.386u,0.005s) (successful) 1 subgoal H : id (fact 8) = fact 8 H0 : id (fact 9) = fact 9 ============================ True
Note that behavior will be the same if you mark
id
asOpaque
because while most reduction tactics refuse to unfoldOpaque
constants, conversion treatsOpaque
as merely a hint to unfold this constant last.We can get around this issue by using
with_strategy
: Goal True.
 1 subgoal ============================ True
 Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity.
 The command has indeed failed with message: Timeout!
 Time assert (id (fact 100) = fact 100) by with_strategy 1 [id] reflexivity.
 Finished transaction in 0.002 secs (0.002u,0.s) (successful) 1 subgoal H : id (fact 100) = fact 100 ============================ True
However, when we go to close the proof, we will run into trouble, because the reduction strategy changes are local to the tactic passed to
with_strategy
. exact I.
 No more subgoals.
 Timeout 1 Defined.
 Toplevel input, characters 018: > Timeout 1 Defined. > ^^^^^^^^^^^^^^^^^^ Error: Timeout!
We can fix this issue by using
abstract
: Goal True.
 1 subgoal ============================ True
 Time assert (id (fact 100) = fact 100) by with_strategy 1 [id] abstract reflexivity.
 Finished transaction in 0.005 secs (0.001u,0.003s) (successful) 1 subgoal H : id (fact 100) = fact 100 ============================ True
 exact I.
 No more subgoals.
 Time Defined.
 Finished transaction in 0.002 secs (0.u,0.s) (successful)
On small examples this sort of behavior doesn't matter, but because Coq is a superlinear performance domain in so many places, unless great care is taken, tactic automation using
with_strategy
may not be robustly performant when scaling the size of the input.Warning
In much the same way this tactic does not play well with
Qed
andDefined
without usingabstract
as an intermediary, this tactic does not play well withcoqchk
, even when used withabstract
, due to the inability of tactics to persist information about conversion hints in the proof term. See #12200 for more details.
Conversion tactics applied to hypotheses¶

Tactic
tactic in ident+,
Applies
tactic
(any of the conversion tactics listed in this section) to the hypothesesident+
.If
ident
is a local definition, thenident
can be replaced bytype of ident
to address not the body but the type of the local definition.Example:
unfold not in (type of H1) (type of H3)
.