Matita Home

`justification let x:t such that p (id)`

- Synopsis:
*justification***let***id***:***term***such that***term***(***id***)**- Pre-condition:
- Action:
It derives

**∃x:t.p**using the**justification**and then it introduces in the context**x**and the hypothesis**p**labelled with**id**.- New sequent to prove:
None.