DEFINITION eq_ind()
TYPE =
       ∀A:Set.∀x:A.∀P:A→Prop.(P x)→∀a:A.(eq A x a)→(P a)
BODY =
        assume A: Set
        assume x: A
        assume P: A→Prop
        suppose H: P x
        assume a: A
        suppose H1: eq A x a
          by cases on H1 we prove P a
             case refl_equal ⇒
                the thesis becomes the hypothesis H
          we proved P a
       we proved ∀A:Set.∀x:A.∀P:A→Prop.(P x)→∀a:A.(eq A x a)→(P a)