Commit 751f6d75 authored by Dan Frumin's avatar Dan Frumin

Strengthen `bin_log_related_weaken_2`

parent d0a6e8d0
...@@ -48,9 +48,9 @@ Section properties. ...@@ -48,9 +48,9 @@ Section properties.
rewrite /env_subst. rewrite !Closed_subst_p_id. done. rewrite /env_subst. rewrite !Closed_subst_p_id. done.
Qed. Qed.
Lemma bin_log_related_weaken_2 τi Δ Γ e1 e2 (τ : type) : Lemma bin_log_related_weaken_2 τi E Δ Γ e1 e2 (τ : type) :
{Δ;Γ} e1 log e2 : τ - {E;Δ;Γ} e1 log e2 : τ -
{τi::Δ;⤉Γ} e1 log e2 : τ.[ren (+1)]. {E;τi::Δ;⤉Γ} e1 log e2 : τ.[ren (+1)].
Proof. Proof.
rewrite bin_log_related_eq /bin_log_related_def. rewrite bin_log_related_eq /bin_log_related_def.
iIntros "Hlog" (vvs ρ) "#Hs #HΓ". iIntros "Hlog" (vvs ρ) "#Hs #HΓ".
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