proposition: Lemma all_belongs_update_inv : forall xs E F, xs ⊂ (E ::= F) -> xs ⊂ E.
proof: Proof. unfold all_belongs; intros xs E F Hincl x Hin. apply Hincl in Hin. apply belongs_update_inv with F; auto. Qed.
imports: Utf8 Equalities