proposition: Lemma Prf_E1_law1 : Equalizer_law1 k E1_mor.
proof: Proof. unfold Equalizer_law1, Equalizer_eq, E1_mor in |- *. intros i j. apply Trans with (Limiting_cone l PA2). apply (EqC1 (Limiting_cone l) (PA_f i)). apply (EqC (Limiting_cone l) (PA_f j)). Qed.
imports: Equalizers PA Limit