proposition: Lemma PA_12_ind : forall P : PA_mor PA1 PA2 -> Prop, (forall i : I, P (PA_f i)) -> forall x : PA_mor PA1 PA2, P x.
proof: Proof. intros P Pf x. change (PA_12_P P x) in |- *. apply (PA_mor_ind (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_12_P P f)); simpl in |- *. trivial. trivial. exact Pf. Qed.
imports: BasicTypes Category