Rocq <
Rocq < Rocq < 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 <
Rocq < Rocq < 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 <
Rocq < Rocq <
Rocq < P1 is declared
P2 is declared
P3 is declared
P4 is declared
Rocq < p12 is declared
Rocq < p123 is declared
Rocq < p34 is declared
Rocq < Rocq < 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 < Second proof:
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 < 1 focused goal (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 goals (shelved: 2)
goal 1 is:
?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:)
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 <
Rocq <
Rocq <
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
