Commit ff87776b authored by Robbert Krebbers's avatar Robbert Krebbers

Add lemma `subst_map_binder_insert_2`.

parent 5088d5b0
......@@ -187,6 +187,15 @@ Lemma subst_map_binder_insert b v vs e :
subst_map (binder_insert b v vs) e =
subst' b v (subst_map (binder_delete b vs) e).
Proof. destruct b; rewrite ?subst_map_insert //. Qed.
Lemma subst_map_binder_insert_2 b1 v1 b2 v2 vs e :
subst_map (binder_insert b1 v1 (binder_insert b2 v2 vs)) e =
subst' b2 v2 (subst' b1 v1 (subst_map (binder_delete b2 (binder_delete b1 vs)) e)).
destruct b1 as [|s1], b2 as [|s2]=> /=; auto using subst_map_insert.
rewrite subst_map_insert. destruct (decide (s1 = s2)) as [->|].
- by rewrite delete_idemp subst_subst delete_insert_delete.
- by rewrite delete_insert_ne // subst_map_insert subst_subst_ne.
(* subst_map on closed expressions *)
Lemma subst_map_is_closed X e vs :
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