writing and applying axioms

Stream: new members

[SparkleOyster]

WX20190326-1850562x.png 1553640646699.jpg

As I'm trying to apply the highlighted hypothesis to this axiom I have written, I noticed that the axiom would only take arguments like individual p or q, instead of the whole Prop \not a = b. Is there a way for me to word it so that I can direct apply my hypothesis as in "exact I1 hb1"?

[Chris Hughes]

I guess you have variables (p q : point) somewhere? Change the brackets to {} , and it will expect ¬p=q as the first argument.

[SparkleOyster]

I guess you have variables (p q : point) somewhere? Change the brackets to {} , and it will expect ¬p=q as the first argument.

Worked! Thank you!