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