Commit d2b71e0a authored by Robbert Krebbers's avatar Robbert Krebbers

Instantiate foralls behind boxes by removing those.

That's like what we are doing when instantiating an arrow or wand.
parent bb5e21f2
Pipeline #2926 passed with stage
in 9 minutes and 55 seconds
......@@ -787,6 +787,9 @@ Global Instance forall_specialize_cons A As x xs Φ (Ψ : A → himpl As (uPred
( x, ForallSpecialize xs (Φ x) (Ψ x))
ForallSpecialize (hcons x xs) ( x : A, Φ x) Ψ.
Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.
Global Instance forall_specialize_always As xs P (Ψ : himpl As (uPred M)) :
ForallSpecialize xs P Ψ ForallSpecialize xs ( P) Ψ | 101.
Proof. rewrite /ForallSpecialize=> ->. by rewrite always_elim. Qed.
Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
envs_lookup i Δ = Some (p, P) ForallSpecialize xs P Φ
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment