Coq < 
Coq < Coq < 1 goal
  
  ============================
  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R

(dependent evars: ; in current goal:)

strange_imp_trans < 
strange_imp_trans < No more goals.

(dependent evars: ; in current goal:)

strange_imp_trans < 
Coq < Coq < 1 goal
  
  ============================
  forall P Q : Prop, (P -> Q) /\ P -> Q

(dependent evars: ; in current goal:)

modpon < 
modpon < No more goals.

(dependent evars: ; in current goal:)

modpon < 
Coq < Coq < 
Coq < P1 is declared
P2 is declared
P3 is declared
P4 is declared

Coq < p12 is declared

Coq < p123 is declared

Coq < p34 is declared

Coq < Coq < 1 goal
  
  P1, P2, P3, P4 : Prop
  p12 : P1 -> P2
  p123 : (P1 -> P2) -> P3
  p34 : P3 -> P4
  ============================
  P4

(dependent evars: ; in current goal:)

p14 < 
p14 < 4 focused goals
(shelved: 2)
  
  P1, P2, P3, P4 : Prop
  p12 : P1 -> P2
  p123 : (P1 -> P2) -> P3
  p34 : P3 -> P4
  ============================
  ?Q -> P4

goal 2 is:
 ?P -> ?Q
goal 3 is:
 ?P -> ?Q
goal 4 is:
 ?P

(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)

p14 < 3 focused goals
(shelved: 2)
  
  P1, P2, P3, P4 : Prop
  p12 : P1 -> P2
  p123 : (P1 -> P2) -> P3
  p34 : P3 -> P4
  ============================
  ?P -> (?P0 -> P4) /\ ?P0

goal 2 is:
 ?P -> (?P0 -> P4) /\ ?P0
goal 3 is:
 ?P

(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11)

p14 < 
Coq < 
Coq <