proposition: Lemma Comp_PA_fact1 : forall (f : PA_mor PA1 PA1) (x : PA_ob) (g : PA_mor PA1 x), Comp_PA_mor f g =_S g.
proof: Proof. intros f x g; apply (PA_11_ind (P:=fun x' : PA_mor PA1 PA1 => Comp_PA_mor x' g =_S g)). generalize g. elim x. simpl in |- *; auto. intro g1; apply Refl. Qed.
imports: BasicTypes Category