Commit 26dc475b authored by Robbert Krebbers's avatar Robbert Krebbers

Add lemma `subst_map_singleton`.

parent 962637df
......@@ -183,6 +183,10 @@ Proof.
+ by rewrite /= binder_delete_insert // delete_insert_delete
!binder_delete_delete delete_idemp.
Qed.
Lemma subst_map_singleton x v e :
subst_map {[x:=v]} e = subst x v e.
Proof. by rewrite subst_map_insert delete_empty subst_map_empty. Qed.
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).
......
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