DEFINITION leq_sym()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.(leq g a1 a2)→(leq g a2 a1)
BODY =
        assume g: G
        assume a1: A
        assume a2: A
        suppose H: leq g a1 a2
          we proceed by induction on H to prove leq g a2 a1
             case leq_sort : h1:nat h2:nat n1:nat n2:nat k:nat H0:eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k) ⇒
                the thesis becomes leq g (ASort h2 n2) (ASort h1 n1)
                   by (sym_eq . . . H0)
                   we proved eq A (aplus g (ASort h2 n2) k) (aplus g (ASort h1 n1) k)
                   by (leq_sort . . . . . . previous)
leq g (ASort h2 n2) (ASort h1 n1)
             case leq_head : a3:A a4:A :leq g a3 a4 a5:A a6:A :leq g a5 a6 ⇒
                the thesis becomes leq g (AHead a4 a6) (AHead a3 a5)
                (H1) by induction hypothesis we know leq g a4 a3
                (H3) by induction hypothesis we know leq g a6 a5
                   by (leq_head . . . H1 . . H3)
leq g (AHead a4 a6) (AHead a3 a5)
          we proved leq g a2 a1
       we proved ∀g:G.∀a1:A.∀a2:A.(leq g a1 a2)→(leq g a2 a1)