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 =
λA:Set
         .λx:A
           .λP:A
                   →(Type:145:cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq_rect.con)
             .λ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