proposition: Lemma PULB_13_rect : forall (P : PULB_mor P1 P3 -> Type) (x : PULB_mor P1 P3), P x.
proof: Proof. intros P x. change (PULB_13_T P x) in |- *. apply (PULB_mor_rect (P:=fun (a b : PULB_ob) (f : PULB_mor a b) => PULB_13_T P f)); simpl in |- *; auto. Qed.
imports: Category BasicTypes