proposition: Lemma FMd_comp_prop : Equal f (comp_hom (FMd_lift:Hom (FreeModule:SET) Mod) FMd_var).
proof: Proof. simpl in |- *. red in |- *. red in |- *. simpl in |- *. intros x; try assumption. exact (Refl (f x)). Qed.
imports: Module_util Module_facts