we have
Prev Chapter 8. Declarative Tactics Next

we have

justification we have t1 (id1) and t2 (id2)

Synopsis:

justification we have term ( id ) and term ( id )

Pre-condition:

Action:

It derives t1∧t2 using the justification then it introduces in the context t1 labelled with id1 and t2 labelled with id2.

New sequent to prove:

None.

Prev Up Next
we need to prove Home we proceed by cases on