suppose term ( id ) [ that is equivalent to term ]

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).

It adds to the context of the current sequent to prove a new declaration x : T . The new conclusion becomes P.

None.