proposition: Lemma PA_21_rect : forall (P : PA_mor PA2 PA1 -> Type) (x : PA_mor PA2 PA1), P x.
proof: Proof. intros P x. change (PA_21_T P x) in |- *. apply (PA_mor_rect (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_21_T P f)); simpl in |- *; auto. Qed.
imports: BasicTypes Category