Skip to content

GitLab

Commit 0b949f98 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Fix issue #141.

parent aaf62d5e
Hide whitespace changes
Inline Side-by-side
Showing with 9 additions and 0 deletions
theories/proofmode/class_instances.v
View file @ 0b949f98
......@@ -170,11 +170,20 @@ Proof. by rewrite /FromAlways. Qed.
Global Instance into_laterN_later n P Q :
IntoLaterN n P Q → IntoLaterN' (S n) (▷ P) Q.
Proof. by rewrite /IntoLaterN' /IntoLaterN =>->. Qed.
Global Instance into_laterN_later_further n P Q :
IntoLaterN' n P Q → IntoLaterN' n (▷ P) (▷ Q).
Proof. rewrite /IntoLaterN' /IntoLaterN =>->. by rewrite -laterN_later. Qed.
Global Instance into_laterN_laterN n P : IntoLaterN' n (▷^n P) P.
Proof. done. Qed.
Global Instance into_laterN_laterN_plus n m P Q :
IntoLaterN m P Q → IntoLaterN' (n + m) (▷^n P) Q.
Proof. rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite laterN_plus. Qed.
Global Instance into_laterN_laterN_further n m P Q :
IntoLaterN' m P Q → IntoLaterN' m (▷^n P) (▷^n Q).
Proof.
rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite -!laterN_plus Nat.add_comm.
Qed.
Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
......
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