proposition: Lemma env_ind : forall (P : gen_env A -> Prop), (P (@empty A)) -> (forall E x v, P E -> P (E & (x ∶ v))) -> (forall E, P E).
proof: Proof. unfold concat, single, singles. induction E as [ | (x, v) ]; simpl in *; auto. Qed.
imports: Utf8 Equalities