proposition: Lemma env_ind : forall (P : env A -> Prop), (P empty) -> (forall E x v, P E -> P (E & x ~ v)) -> (forall E, P E).
proof: Proof. Proof using. rew_env_defs. induction E as [|(x,v)]. auto. applys_eq* H0. rew_list*. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)