blob: 5a59054073b3fb8b7cdd4303473ca51261f78c1a (
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
|
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.
eapply strange_imp_trans.
apply modpon.
Abort.
End eex.
|
