proposition: Theorem all_binds_update : forall A (E F G : gen_env A), E ⊏ F -> (E ::= G) ⊏ (F ::= G).
proof: Proof. intros A E F G Habind. unfold all_binds in *. intros x v Hbind. apply binds_update_inv in Hbind. destruct Hbind as [ [ Hnotin Hbind ] | [ Hin Hbind ] ]. apply binds_update_notin; auto. apply belongs_binds in Hin. destruct Hin as [ w Hbind2 ]. apply Habind in Hbind2. apply binds_belongs in Hbind2. apply binds_update_in; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv