blob: 5e61529b4b2136700dae3ba5076330a7c04b3f56 (
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.
|