blob: d0f3a4012e6ec4a17ef628d717bffc7745776e94 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
Set Printing Dependent Evars Line.
Lemma strange_imp_trans :
forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
Proof.
auto.
Qed.
Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
Proof.
tauto.
Qed.
Section eex.
Variables P1 P2 P3 P4 : Prop.
Hypothesis p12 : P1 -> P2.
Hypothesis p123 : (P1 -> P2) -> P3.
Hypothesis p34 : P3 -> P4.
Lemma p14 : P4.
Proof.
idtac "Second proof:".
eapply strange_imp_trans.
{
apply modpon.
}
Abort.
End eex.
|
