Matita Home

`suppose t1 (x) that is equivalent to t2`

- Synopsis:
- Pre-condition:
The conclusion of the current proof must be

**∀x:T.P**or**T→P**where**T**is a proposition (i.e.**T**has type**Prop**or**CProp**).- Action:
It adds to the context of the current sequent to prove a new declaration

**x : T**. The new conclusion becomes**P**.- New sequents to prove:
None.