proposition: Theorem binds_singles_inv : forall A x y (v w : A) ys (ws : list A), x ∹ v ⋲ (y :: ys ∷ w :: ws) -> (x = y ∧ v = w) ∨ (x ∹ v ⋲ (ys ∷ ws)).
proof: Proof. intros A x y v w ys ws Hbind. inversion Hbind as [ Hget ]. rewrite singles_cons in Hget. apply get_concat_inv in Hget. destruct Hget as [ Heq | Hneq ]. left. destruct Heq; split; auto. right. destruct Hneq. auto. Qed.
imports: Utf8 Equalities CoreGenericEnv