proposition: Theorem all_binds_single_singles : forall A x y (v w : A) ys (ws : list A), x = y -> v = w -> (x ∶ v) ⊏ (y :: ys ∷ w :: ws).
proof: Proof. intros. apply binds_all_binds. apply binds_singles; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv