Title: A first example of well orderings in type theory