fact: Definition Equal_PA_mor (x y : PA_ob) (f g : PA_mor x y) := match f in (PA_mor x' y') return Prop with | PA_I1 => True | PA_I2 => True | PA_f i => match g in (PA_mor x' y') return Prop with | PA_I1 => False | PA_I2 => False | PA_f j => k i =_S k j end end.
imports: BasicTypes Category