proposition: Theorem all_binds_single_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 Habind. apply all_binds_binds in Habind. apply binds_singles_inv in Habind. destruct Habind; [ left | right ]; auto. apply binds_all_binds; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv