Skip to content

GitLab

Commit e4091905 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Do not use automatically generated name.

parent e2bb6d8d
Hide whitespace changes
Inline Side-by-side
theories/base_logic/upred.v
View file @ e4091905
...@@ -509,7 +509,7 @@ Proof. ...@@ -509,7 +509,7 @@ Proof.
intros P Q. intros P Q.
unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S]. unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
- (* P ⊢ ▷ P *) - (* P ⊢ ▷ P *)
intros P. unseal; split=> n x ? HP. destruct n; first done. simpl. intros P. unseal; split=> -[|n] /= x ? HP; first done.
apply uPred_mono with (S n) x; eauto using cmra_validN_S. apply uPred_mono with (S n) x; eauto using cmra_validN_S.
- (* (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a *) - (* (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a *)
intros A Φ. unseal; by split=> -[|n] x. intros A Φ. unseal; by split=> -[|n] x.
......
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