Table of Contents
absurd P
P must have type Prop.
It closes the current sequent by eliminating an absurd term.
It opens two new sequents of conclusion P and ¬P.
Matita HomeMatita Home