[TYPES] A geometry problem for proof systems

[Peter Freyd]

Yong Lua asks if the following is a theorem:

  A triangle with two internal angle bisectors of equal length is
  an isosceles triangle.

When I was asked this by a fellow high school student (thousands of
years ago) I gave him a long, quite ugly, computational proof (which
did not, alas, satisfy her notion of proof).

I've never seen a proof other than the ugly one.

These days, of course, one just asks Google. The query:

   angle bisector isosceles

leads one to 

   www.mathpages.com/home/kmath433.htm

It has the ugly proof.

   Peter