The documentation says
Existential variables can be named by the user upon creation using the syntax ?[ident].
What does this mean? Specifically, where the existential is created by
eapply nrs_rule_indep in n.
eapply nrs_rule_indep in n as ?[xxx].
eapply nrs_rule_indep in n ?[xxx].
neither works. How do I name the existential that is created?
There’s some room for improvement in the docs. You can directly apply a lemma to an existential variable (
eapply (nrs_rule_indep ?[xxx])) or use the
eapply _ with syntax (
eapply nrs_rule_indep with (x := ?[xxx]), if
nrs_rule_indep is a function with first argument named
nrs_rule_indep : forall (x : _), ...).
Here are some more example usages with
Parameter prop : forall n : nat, True -> n = n.
Goal True -> exists n : nat, n = S n.
eapply prop with (n := ?[x] + ?x) in H.
(* H : ?x + ?x = ?x + ?x *)
(* Goal : ?y = S ?y*)
Hi Li-yao - thanks for that,