proposition: Lemma all_belongs_update_one_inv : forall x xs v E, xs ⊂ (E [x <- v]) -> xs ⊂ E.
proof: Proof. intros x xs v E Hin. unfold all_belongs in Hin |- *. intros y Hin2. apply Hin in Hin2. apply belongs_update_one_inv with x v; auto. Qed.
imports: Utf8 Equalities