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)

    construct [L] : (line(L) & inc_po_l(B,L) & inc_po_l(C,L))
    infer (col(A,B,C))
    lookup contradiction

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

