ffun aT -> rT}) : f1 =1 f2 <-> f1 = f2.
Admitted.

(* This is the context one needs in order to type check the lemma, it's an
extract of bigop.v *)
Section Distributivity.

Import Monoid.Theory.

Variable R : Type.
Variables zero one : R.
Local Notation "0" := zero.
Local Notation "1" := one.
Variable times : Monoid.mul_law 0.
Local Notation "*%M" := times (at level 0).
Local Notation "x * y" := (times x y).
Variable plus : Monoid.add_law 0 *%M.
Local Notation "+%M" := plus (at level 0).
Local Notation "x +