justification let id : term such that term ( id )

None.

It applies the left introduction rule of the existential quantifier on the formula ∃ x. P(x) (in Natural Deduction this corresponds to the elimination rule for the quantifier).

A new sequent with ∃ x. P(x) as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses x : T and H : P are added to the context.