Dear community,

I would like to create an Ltac2 function that does the equivalent of the following Coq tactics:

`pose (ident := constr); exists ident.`

An example of the above would be when proving a trivial statement of the form

`forall n , exists m, n = m `

I know that I can use the `pose`

function from the Ltac2 `Std.v`

file as `Std.pose (Some s) t`

, but I do not know how to continue from here, as `Std.pose (Some s) t`

is now of type `unit`

, and the `exists`

tactic from the Ltac2 `Notations.v`

file takes as input a binding.