proposition: Lemma PA_22_ind : forall P : PA_mor PA2 PA2 -> Prop, P PA_I2 -> forall x : PA_mor PA2 PA2, P x.
proof: Proof. intros P PP2 x. change (PA_22_P P x) in |- *. apply (PA_mor_ind (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_22_P P f)); simpl in |- *. trivial. exact PP2. trivial. Qed.
imports: BasicTypes Category