proposition: Lemma S_eta_rule : Eta_rule_law (C1:=SET_hasBinProd) S_eval S_Lambda.
proof: Proof. unfold Eta_rule_law in |- *; simpl in |- *. intros C h; unfold Ext in |- *; simpl in |- *. intro c; unfold Ext in |- *; simpl in |- *. intro a; unfold S_eval_fun in |- *; simpl in |- *. unfold Comp_fun in |- *; simpl in |- *. apply Pres1. apply Refl. Qed.
imports: SET_BinProds Exponents