DEFINITION eq_rect()
TYPE =
       ΠA:Set
         .Πx:A
           .ΠP:A
                    →(Type:145:cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_rect.con)
             .(P x)→Πa:A.(eq A x a)→(P a)
BODY =
Show proof