DEFINITION and3_rect()
TYPE =
       ΠP0:Prop
         .ΠP1:Prop
           .ΠP2:Prop
             .ΠP:(Type:46843:cic:/matita/LAMBDA-TYPES/Base-1/types/defs/and3_rect.con)
               .(P0→P1→P2→P)→(and3 P0 P1 P2)→P
BODY =
λP0:Prop
         .λP1:Prop
           .λP2:Prop
             .λP:(Type:46843:cic:/matita/LAMBDA-TYPES/Base-1/types/defs/and3_rect.con)
               .λf:P0→P1→P2→P.λH:and3 P0 P1 P2.<λH1:and3 P0 P1 P2.P> CASE H OF and3_intro H1 H2 H3⇒f H1 H2 H3