Commit 446bc644 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More `subst_map` lemmas.

parent 250a2dd8
......@@ -187,6 +187,10 @@ 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_empty b v e :
subst_map (binder_insert b v ) e = subst' b v e.
Proof. by rewrite subst_map_binder_insert binder_delete_empty subst_map_empty. 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)).
......@@ -196,6 +200,12 @@ Proof.
- by rewrite delete_idemp subst_subst delete_insert_delete.
- by rewrite delete_insert_ne // subst_map_insert subst_subst_ne.
Lemma subst_map_binder_insert_2_empty b1 v1 b2 v2 e :
subst_map (binder_insert b1 v1 (binder_insert b2 v2 )) e =
subst' b2 v2 (subst' b1 v1 e).
by rewrite subst_map_binder_insert_2 !binder_delete_empty subst_map_empty.
(* subst_map on closed expressions *)
Lemma subst_map_is_closed X e vs :
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