DEFINITION eq_rec()
TYPE =
       ΠA:Set
         .Πx:A.ΠP:A→Set.(P x)→Πa:A.(eq A x a)→(P a)
BODY =
Show proof