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