blob: 7b430ace5ebcf0ad234f4920c4ff473ab11c7848 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Require Import Setoid Program.Basics.
Parameter P : nat -> Prop.
Parameter R : nat -> nat -> Prop.
Add Parametric Morphism : P
with signature R ++> impl as PM1.
Admitted.
Add Parametric Morphism : P
with signature R --> impl as PM2.
Admitted.
Goal forall x y, R x y -> P y -> P x.
Proof.
intros x y H1 H2.
rewrite H1.
auto.
Qed.
|
