proposition: Lemma PULB_21_T : (PULB_mor P2 P1 -> Type) -> forall a b : PULB_ob, PULB_mor a b -> Type.
proof: Proof. intros P a b; elim a; elim b. intro x; exact UnitType. intro x; exact UnitType. intro x; exact UnitType. exact P. intro x; exact UnitType. intro x; exact UnitType. intro x; exact UnitType. intro x; exact UnitType. intro x; exact UnitType. Defined.
imports: Category BasicTypes