proposition: Lemma Idr_PA : Idr_law Comp_PA Id_PA.
proof: Proof. unfold Idr_law in |- *; simpl in |- *. intros x y f; elim f. apply (Comp_PA_fact1 PA_I1 PA_I1). apply (Comp_PA_fact2 PA_I2 PA_I2). intro i; apply (Comp_PA_fact3 i PA_I2). Qed.
imports: BasicTypes Category