DEFINITION unintro()
TYPE =
       ∀A:Set.∀a:A.∀P:A→Prop.(∀x:A.(P x))→(P a)
BODY =
        assume A: Set
        assume a: A
        assume P: A→Prop
        suppose H: ∀x:A.(P x)
          by (H .)
          we proved P a
       we proved ∀A:Set.∀a:A.∀P:A→Prop.(∀x:A.(P x))→(P a)