proposition: Lemma S_beta_rule : Beta_rule_law (C1:=SET_hasBinProd) S_eval S_Lambda.
proof: Proof. unfold Beta_rule_law in |- *; simpl in |- *. intros C f; unfold Ext in |- *; simpl in |- *. intro cxa; unfold S_eval_fun in |- *; simpl in |- *. unfold S_lambda_fun2 in |- *. apply Pres1. simpl in |- *; unfold Equal_Sprod in |- *; simpl in |- *; split. apply Refl. unfold Id_fun in |- *; apply Refl. Qed.
imports: SET_BinProds Exponents