proposition: Lemma fmult_eq_compat : forall A k1 k2 (f1 f2:MF A), k1==k2 -> f1==f2 -> fmult k1 f1 == fmult k2 f2.
proof: Proof. intros; simpl; apply ford_eq_intro; intro x. repeat (rewrite fmult_eq); firstorder. Qed.
imports: ALEA(Utheory)