proposition: Lemma Comp_PA_congl : Congl_law Comp_PA_mor.
proof: Proof. unfold Congl_law in |- *. intros x y z f g h. generalize f; generalize g. elim h; elim z. simpl in |- *; auto. simpl in |- *; auto. intros f0 g0 H. apply (PA_21_ind (fun x : PA_mor PA2 PA1 => Comp_PA_mor PA_I2 g0 =_S Comp_PA_mor PA_I2 f0) g0). simpl in |- *; auto. intros i g0 f0 H. apply (PA_21_ind (fun x : PA_mor PA2 PA1 => Comp_PA_mor (PA_f i) f0 =_S Comp_PA_mor (PA_f i) g0) f0). intros i g0 f0 H; apply Refl. Qed.
imports: BasicTypes Category