proposition: Lemma includedin_update : forall (A : Type) (m m' : partial_map A) (x : string) (vx : A), includedin m m' -> includedin (x |-> vx ; m) (x |-> vx ; m').
proof: Proof. unfold includedin. intros A m m' x vx H. intros y vy. destruct (eqb_spec x y) as [Hxy | Hxy]. - rewrite Hxy. rewrite update_eq. rewrite update_eq. intro H1. apply H1. - rewrite update_neq. rewrite update_neq. + apply H. + apply Hxy. + apply Hxy. Qed.
imports: Coq(Arith.Arith) Coq(Bool.Bool) Coq.Strings.String Coq(Logic.FunctionalExtensionality) Coq(Lists.List)