DEFINITION leq_refl()
TYPE =
       ∀g:G.∀a:A.(leq g a a)
BODY =
        assume g: G
        assume a: A
          we proceed by induction on a to prove leq g a a
             case ASort : n:nat n0:nat ⇒
                the thesis becomes leq g (ASort n n0) (ASort n n0)
                   by (refl_equal . .)
                   we proved eq A (aplus g (ASort n n0) O) (aplus g (ASort n n0) O)
                   by (leq_sort . . . . . . previous)
leq g (ASort n n0) (ASort n n0)
             case AHead : a0:A a1:A ⇒
                the thesis becomes leq g (AHead a0 a1) (AHead a0 a1)
                (H) by induction hypothesis we know leq g a0 a0
                (H0) by induction hypothesis we know leq g a1 a1
                   by (leq_head . . . H . . H0)
leq g (AHead a0 a1) (AHead a0 a1)
          we proved leq g a a
       we proved ∀g:G.∀a:A.(leq g a a)