proposition: Lemma all_remove_update : forall xs E F, ok E -> (E ::= F) ∖ xs = (E ∖ xs) ::= F.
proof: Proof. intros xs E F. generalize E. clear E. induction xs as [ | x xs IHxs ]; intros; simpl; auto. rewrite remove_update; auto. apply IHxs. apply ok_remove; auto. Qed.
imports: Utf8 Equalities