proposition: Lemma Comp_PA_congr : Congr_law Comp_PA_mor.
proof: Proof. unfold Congr_law in |- *. intros x y z f; elim f. intro g; lapply (PA_11_ind (P:=fun x' : PA_mor PA1 PA1 => forall h : PA_mor PA1 z, PA_I1 =_S x' -> Comp_PA_mor PA_I1 h =_S Comp_PA_mor x' h)). intros H h H0; apply (H g h H0). elim z. simpl in |- *; auto. intros h H; apply Refl. intro g; lapply (PA_22_ind (P:=fun x' : PA_mor PA2 PA2 => forall h : PA_mor PA2 z, Equal_PA_mor PA_I2 x' -> Comp_PA_mor PA_I2 h =_S Comp_PA_mor x' h)). intros H h H0; apply (H g h H0). elim z. intros h H; apply (PA_21_ind (fun x' : PA_mor PA2 PA1 => Comp_PA_mor PA_I2 h =_S Comp_PA_mor PA_I2 h) h). simpl in |- *; auto. intros i g; lapply (PA_12_ind (P:=fun x' : PA_mor PA1 PA2 => forall h : PA_mor PA2 z, Equal_PA_mor (PA_f i) x' -> Comp_PA_mor (PA_f i) h =_S Comp_PA_mor x' h)). intros H h H0; apply (H g h H0). elim z. intros j h H; apply (PA_21_ind (fun x' : PA_mor PA2 PA1 => Comp_PA_mor (PA_f i) h =_S Comp_PA_mor (PA_f j) h) h). intros j h H; simpl in |- *; exact H. Qed.
imports: BasicTypes Category