Proof that two lines intersect each other at precisely one point in Idris
It still may be far from perfect, but I asked a question on Stackoverflow related to this, and received an excellent answer from xash.

I have attempted to cure my Boolean blindness. If I understand correctly, the operator == asks the question "Is the left hand side equal to the right hand side?" Instead, I want to say: "I have a proof that this holds." 

To fix this, I changed a lot of my functions like colinear to more closely match the (=) signature:

colinear : point -&gt; point -&gt; point -&gt; Bool


becomes:

Colinear : point -&gt; point -&gt; point -&gt; Type


Also, I removed a /= b and instead replaced it with Not (a = b).

Here was the resulting code:

interface Plane line point where 
  -- Abstract notion for saying three points lie on the same line.
  Colinear : point -&gt; point -&gt; point -&gt; Type
  Coplanar : point -&gt; point -&gt; point -&gt; Type
  Contains : line -&gt; point -&gt; Type

  -- Intersection between two lines
  IntersectsAt : line -&gt; line -&gt; point -&gt; Type

  -- If two lines l and m contain a point a, they intersect at that point.
  intersection_criterion : (l : line) -&gt; 
                           (m : line) -&gt;
                           (a : point) -&gt;
                           Contains l a -&gt; 
                           Contains m a -&gt; 
                           IntersectsAt l m a

  -- If l and m intersect at a point a, then they both contain a.
  intersection_result : (l : line) -&gt;
                        (m : line) -&gt;
                        (a : point) -&gt;
                        IntersectsAt l m a -&gt;
                        (Contains l a, Contains m a)

  -- For any two distinct points there is a line that contains them.
  line_contains_two_points : (a : point) -&gt; 
                             (b : point) -&gt;
                             Not (a = b) -&gt;
                             (l : line ** (Contains l a, Contains l b))

  -- If two points are contained by l and m then l = m
  two_pts_define_line : (l : line) -&gt;
                        (m : line) -&gt;
                        (a : point) -&gt;
                        (b : point) -&gt;
                        Not (a = b) -&gt;
                        Contains l a -&gt;
                        Contains l b -&gt;
                        Contains m a -&gt; 
                        Contains m b -&gt; 
                        (l = m)

  same_line_same_pts : (l : line) -&gt;
                       (m : line) -&gt;
                       (a : point) -&gt;
                       (b : point) -&gt;
                       Not (l = m) -&gt;
                       Contains l a -&gt;
                       Contains l b -&gt;
                       Contains m a -&gt;
                       Contains m b -&gt;
                       (a = b)

  -- There exists 3 non-colinear points.
  three_non_colinear_pts : (a : point ** b : point ** c : point ** 
                           (colinear a b c = False, 
                           Not (a = b), 
                           Not (b = c), 
                           Not (a = c)))

  -- Any line contains at least two points.
  contain_two_pts : (l : line) -&gt;
                    (a : point ** b : point ** 
                    (Contains l a, Contains l b))

-- If two lines intersect at a point and they are not identical, that is the o-
-- nly point they intersect at.
intersect_at_most_one_point : Plane line point =&gt;
  (l : line) -&gt; (m : line) -&gt; (a : point) -&gt; (b : point) -&gt;
  Not (l = m) -&gt;
  IntersectsAt l m a -&gt;
  IntersectsAt l m b -&gt;
  (a = b)

intersect_at_most_one_point l m a b l_not_m int_at_a int_at_b =
  same_line_same_pts
  l
  m
  a
  b
  l_not_m
  (fst (intersection_result l m a int_at_a))
  (fst (intersection_result l m b int_at_b))
  (snd (intersection_result l m a int_at_a))
  (snd (intersection_result l m b int_at_b))