DEFINITION eq_ind_r()
TYPE =
       ∀A:Set.∀x:A.∀P:A→Prop.(P x)→∀y:A.(eq A y x)→(P y)
BODY =
        assume A: Set
        assume x: A
        assume P: A→Prop
        suppose H: P x
        assume y: A
        suppose H0: eq A y x
          by (sym_eq . . . H0)
          we proved eq A x y
          by cases on the previous result we prove P y
             case refl_equal ⇒
                the thesis becomes the hypothesis H
          we proved P y
       we proved ∀A:Set.∀x:A.∀P:A→Prop.(P x)→∀y:A.(eq A y x)→(P y)