proposition: Lemma PULB_33_ind : forall P : PULB_mor P3 P3 -> Prop, P IP3 -> forall x : PULB_mor P3 P3, P x.
proof: Proof. intros P Pi1 x. change (PULB_33_P P x) in |- *. apply (PULB_mor_ind (P:=fun (a b : PULB_ob) (f : PULB_mor a b) => PULB_33_P P f)); simpl in |- *. trivial. trivial. exact Pi1. trivial. trivial. Qed.
imports: Category BasicTypes