A,B:Type. ((A inj B))  (f:(AB). Inj(A; B; f))

By:	Def of A inj B THEN UnivCD

1

1. A : Type 2. B : Type   ({f:(AB)| Inj(A; B; f) })  (f:(AB). Inj(A; B; f))

4 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html