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