DEFINITION eq_rec()
TYPE =
       ΠA:Set
         .Πx:A.ΠP:A→Set.(P x)→Πa:A.(eq A x a)→(P a)
BODY =
λA:Set
         .λx:A
           .λP:A→Set
             .λp:P x.λa:A.λH:eq A x a.<λa1:A.λH1:eq A x a1.P a1> CASE H OF refl_equal⇒p