Ssreflect Users Discussion List

[<>]

Hello.

Is there a way to combine "apply [term]" and the move tactic ":"
as in the following example?

Variables a1 a2: nat.
Variable al: nat -> Prop.
Axiom a1a2: al a1 -> al a2.

Goal al a1 -> al a2.
intro h. (apply a1a2): h.

In fact, I could do equivalently:

Goal al a1 -> al a2.
intro h. move: h; apply a1a2

But I prefer the former since it manifests 
that the application of a1a2 consumes h with the consice syntax. 

Furthermore, it would be nice if I could combine "generalize [term]" and move
as in the following example.

Goal al a1 -> al a2.
intro h. (generalize a1a2): h.

The semantics I envisage is:

Goal al a1 -> al a2.
intro h. generalize (a1a2 h); clear h.

While it does not use move, the behavior appears similar to me,
that is, the generalization of a1a2 consumes h. 

I often do forward reasoning where I use this pattern. 
I hope this is not against the design principles of ssr :-)

With best regards,
Keiko