Matita Home

`obtain H t1 = t2 justification`

- Synopsis:
[

**obtain***id*|**conclude***term*]**=***term*[*auto_params*|**using***term*|**using once***term*|**proof**] [**done**]- Pre-condition:
**conclude**can be used only if the current sequent is stating an equality. The left hand side must be omitted in an equality chain.- Action:
Starts or continues an equality chain. If the chain starts with

**obtain H**a new subproof named**H**is started.- New sequent to prove:
If the chain starts with

**obtain H**a nre sequent for**t2 = ?**is opened.