proposition: Lemma fplus_eq_compat : forall A (f1 f2 g1 g2:MF A), f1==f2 -> g1==g2 -> fplus f1 g1 == fplus f2 g2.
proof: Proof. intros; simpl; apply ford_eq_intro; intro x. repeat (rewrite fplus_eq); firstorder. Qed.
imports: ALEA(Utheory)