proposition: Lemma PA_11_ind : forall P : PA_mor PA1 PA1 -> Prop, P PA_I1 -> forall x : PA_mor PA1 PA1, P x.
proof: Proof. intros P PP1 x. change (PA_11_P P x) in |- *. apply (PA_mor_ind (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_11_P P f)); simpl in |- *. exact PP1. trivial. trivial. Qed.
imports: BasicTypes Category