Commit dd987574 authored by Ralf Jung's avatar Ralf Jung

get rid of 2nd into_persistent_intuitionistically instance

parent ee12aa64
......@@ -210,11 +210,13 @@ Global Instance into_persistent_affinely p P Q :
IntoPersistent p P Q IntoPersistent p (<affine> P) Q | 0.
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
Global Instance into_persistent_intuitionistically p P Q :
IntoPersistent p P Q IntoPersistent p ( P) Q | 0.
Proof. rewrite /IntoPersistent /= =><-. by rewrite intuitionistically_elim. Qed.
Global Instance into_persistent_intuitionistically2 P Q :
IntoPersistent true P Q IntoPersistent false ( P) Q | 0.
Proof. rewrite /IntoPersistent /= =><-. by rewrite intuitionistically_persistently_1. Qed.
IntoPersistent true P Q IntoPersistent p ( P) Q | 0.
Proof.
rewrite /IntoPersistent /= =><-.
destruct p; simpl;
eauto using persistently_mono, intuitionistically_elim,
intuitionistically_persistently_1.
Qed.
Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
IntoPersistent p P Q IntoPersistent p P Q | 0.
Proof.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment