# Applying an axiom from a class in a proof

I'm trying to represent Boole-Schroder Algebra in Coq, and am trying to use apply to start a proof using one of my defined axioms, but I'm getting an "unable to unify" error. Why can't I use apply with that axiom?

Class BooleSchroderAlgebra (A : Type) := {
zero : A;  (* null class *)
one : A;  (* universe of discourse class *)
union : A -> A -> A;
inter : A -> A -> A;
neg : A -> A;
contains : A -> A -> Prop;

neg_zero : neg zero = one;
neg_one : neg one = zero;
union_def : forall a b, union a b = neg(inter (neg a) (neg b));
contains_def : forall a b, contains a b -> inter a b = a;

identity : forall a, inter a a = a;
inter_comm : forall a b, inter a b = inter b a;
inter_assoc : forall a b c, inter a (inter b c) = inter (inter a b) c;
inter_zero : forall a, inter a zero = zero;
}.

Theorem inter_neg_zero_contains : forall (A : Type) (BSA : BooleSchroderAlgebra A) (a b : A),
inter a (neg b) = zero -> contains a b.
Proof.
intros A BSA a b H.
apply contains_def.

The error I'm getting:

A : Type
BSA : BooleSchroderAlgebra A
a, b : A
H : inter a (neg b) = zero
Unable to unify "inter ?M826 ?M827 = ?M826" with
"(let
(zero, one, union, inter, neg, contains, _, _, _, _, _, _, _,
_) :=
BSA in
contains)
a
b".
• Aren't you missing some axioms about how intersection and negation interact? And also, how negation interacts with itself (ie, being involutive)? Without this, I don't think you will be able to prove your goal. Commented Jun 19 at 8:36
• It would be more convenient to axiomatize such algebras without union and deifne unions by Definition union a b := neg (inter (neg a) (neg b)). Commented Jun 19 at 16:08