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