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>.
  1. without cut nor assert
  2. with cut
  3. with assert

Solution

See file cut_example.v