justification let x:t such that p (id)
justification let id : term such that term ( id )
It derives ∃x:t.p using the justification and then it introduces in the context x and the hypothesis p labelled with id.
None.
Matita HomeMatita Home