proposition: Lemma Comp_PA_fact4 : forall (i : I) (g : PA_mor PA2 PA1) (h : PA_mor PA1 PA1), Comp_PA_mor (PA_f i) g =_S h.
proof: Proof. intros i g h; apply (PA_21_ind (fun x' : PA_mor PA2 PA1 => Comp_PA_mor (PA_f i) g =_S h) g). Qed.
imports: BasicTypes Category