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