proposition: Lemma PA_22_P : (PA_mor PA2 PA2 -> Prop) -> forall x y : PA_ob, PA_mor x y -> Prop.
proof: Proof. intros P x y; elim x; elim y. intro x'; exact True. intro x'; exact True. intro x'; exact True. exact P. Defined.
imports: BasicTypes Category