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.