DEFINITION xinduction()
TYPE =
       ∀A:Set.∀t:A.∀P:A→Prop.(∀x:A.(eq A t x)→(P x))→(P t)
BODY =
        assume A: Set
        assume t: A
        assume P: A→Prop
        suppose H: ∀x:A.(eq A t x)→(P x)
          by (refl_equal . .)
          we proved eq A t t
          by (H . previous)
          we proved P t
       we proved ∀A:Set.∀t:A.∀P:A→Prop.(∀x:A.(eq A t x)→(P x))→(P t)