proposition: Lemma concat_singles : forall xs1 xs2 vs1 vs2, length xs1 = length vs1 -> length xs2 = length vs2 -> (xs2 ~* vs2) & (xs1 ~* vs1) = (xs1 ++ xs2) ~* (vs1 ++ vs2).
proof: Proof. Proof using. introv E1 E2. rew_env_defs. gen vs1. induction xs1; destruct vs1; intros; tryfalse; rew_listx. rew_list~. rew_list. simpl. rew_list. fequals~. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)