Coq < 
Coq < Coq < 1 subgoal
  
  ============================
  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 subgoals.

(dependent evars: ; in current goal:)

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

(dependent evars: ; in current goal:)

modpon < 
modpon < No more subgoals.

(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 subgoal
  
  P1, P2, P3, P4 : Prop
  p12 : P1 -> P2
  p123 : (P1 -> P2) -> P3
  p34 : P3 -> P4
  ============================
  P4

(dependent evars: ; in current goal:)

p14 < 
p14 < Second proof:

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

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

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

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

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

p14 < This subproof is complete, but there are some unfocused goals.
Try unfocusing with "}".

3 subgoals
(shelved: 2)

subgoal 1 is:
 ?P -> (?Goal2 -> P4) /\ ?Goal2
subgoal 2 is:
 ?P -> (?Goal2 -> P4) /\ ?Goal2
subgoal 3 is:
 ?P

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

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

subgoal 2 is:
 ?P -> (?Goal2 -> P4) /\ ?Goal2
subgoal 3 is:
 ?P

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

p14 < 
Coq < 
Coq <