proposition: Lemma PULB_31_P : (PULB_mor P3 P1 -> Prop) -> forall a b : PULB_ob, PULB_mor a b -> Prop.
proof: Proof. intros P a b; elim a; elim b. intro x; exact True. intro x; exact True. intro x; exact True. intro x; exact True. intro x; exact True. intro x; exact True. exact P. intro x; exact True. intro x; exact True. Defined.
imports: Category BasicTypes