assume [A,B,C] : (point(A) & point(B) & point(C) & ncol(A,B,C))
goal (A != B & B != C & C != A)

infer (A = B | A != B)

case (A = B)

    infer (B = C | B != C)

    case (B = C)
    
    infer (col(A,B,C))
    lookup contradiction

    case (B != C)

    infer (col(A,B,C))
    lookup contradiction

case (A != B)
infer (B!=C & C!=A)
lookup goal

