# Proofs with or without Cut

Consider the following context :
Variables P Q R T : Prop.
Hypothesis H : P -> Q.
Hypothesis H0 : Q -> R.
Hypothesis H1 : (P -> R) -> T -> Q.
Hypothesis H2 : (P -> R) -> T.

Compare the proof terms of `Q` obtained from interactive
manual proofs *without using *`auto>`.
- without
`cut` nor `assert`
- with
`cut`
- with
`assert`

## Solution

See file cut_example.v

Going home

Pierre Castéran