proposition: Theorem all_binds_single_single_inv : forall A x y (v w : A), (x ∶ v) ⊏ (y ∶ w) -> x = y ∧ v = w.
proof: Proof. intros A x y v w Habind. apply all_binds_binds in Habind. apply binds_single_inv; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv