proposition: Lemma Prf_eta_rule1 : Eta_rule_law Eval1 Lambda1.
proof: Proof. unfold Eta_rule_law in |- *; intros c h; simpl in |- *. unfold Lambda1_mor in |- *. apply Sym. apply (Prf_isCoUA_law2 ua' (a':=c) (f:=Mor_prod H h (Id a) o Eval1) (g:=h)). unfold CoUA_eq in |- *. apply Refl. Qed.
imports: Cartesian1 CCC FunProd