proposition: Lemma singles_cons : forall x v xs vs, (x::xs) ~* (v::vs) = (xs ~* vs) & (x ~ v).
proof: Proof. Proof using. intros. rew_env_defs. simpl. rew_env_defs. fequals. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)