proposition: Lemma GEl_prop1 E f: is_law E f -> function_prop (Opfun E f) (E\times E) E.
proof: Proof. rewrite /Opfun => Ho; saw; apply:lf_function => x /setX_P [pa pb pc]. by apply: Ho. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)