(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Automatic Coercions Import.
Set Implicit Arguments.
Unset Strict Implicit.
Require Export Module_util.
Require Export Module_facts.
Section Free_Module_def.
Variable R : RING.
Variable V : SET.

Inductive FMd : Type :=
  | Var : V -> FMd
  | Law : FMd -> FMd -> FMd
  | Unit : FMd
  | Inv : FMd -> FMd
  | Op : R -> FMd -> FMd.

Inductive eqFMd : FMd -> FMd -> Prop :=
  | eqFMd_Var : forall x y : V, Equal x y -> (eqFMd (Var x) (Var y):Prop)
  | eqFMd_law :
      forall x x' y y' : FMd,
      eqFMd x x' -> eqFMd y y' -> (eqFMd (Law x y) (Law x' y'):Prop)
  | eqFMd_law_assoc :
      forall x y z : FMd, eqFMd (Law (Law x y) z) (Law x (Law y z)):Prop
  | eqFMd_law0r : forall x : FMd, eqFMd (Law x Unit) x:Prop
  | eqFMd_inv : forall x y : FMd, eqFMd x y -> eqFMd (Inv x) (Inv y)
  | eqFMd_invr : forall x : FMd, eqFMd (Law x (Inv x)) Unit
  | eqFMd_refl : forall x : FMd, eqFMd x x:Prop
  | eqFMd_sym : forall x y : FMd, eqFMd x y -> (eqFMd y x:Prop)
  | eqFMd_trans :
      forall x y z : FMd, eqFMd x y -> eqFMd y z -> (eqFMd x z:Prop)
  | eqFMd_com : forall x y : FMd, eqFMd (Law x y) (Law y x)
  | eqFMd_op_comp :
      forall (a b : R) (x y : FMd),
      Equal a b -> eqFMd x y -> (eqFMd (Op a x) (Op b y):Prop)
  | eqFMd_oplin_l :
      forall (a b : R) (x : FMd),
      eqFMd (Op (sgroup_law R a b) x) (Law (Op a x) (Op b x))
  | eqFMd_oplin_r :
      forall (a : R) (x y : FMd),
      eqFMd (Op a (Law x y)) (Law (Op a x) (Op a y))
  | eqFMd_op_assoc :
      forall (a b : R) (x : FMd),
      eqFMd (Op a (Op b x)) (Op (ring_mult a b) x)
  | eqFMd_op_unit : forall x : FMd, eqFMd (Op (ring_unit R) x) x.
Hint Resolve eqFMd_Var eqFMd_law eqFMd_law_assoc eqFMd_law0r eqFMd_invr
  eqFMd_refl: algebra.
Hint Immediate eqFMd_sym: algebra.

Lemma eqFMd_Equiv : equivalence eqFMd.
(* Goal: forall x : Carrier V, @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f x) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@comp_hom SET V FMd_set (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@f2 (@G FMd_set Law Unit Inv eqFMd_law eqFMd_law_assoc eqFMd_law0r eqFMd_inv eqFMd_invr) (abelian_group_group (@module_carrier R Mod)) FMd_lift_fun (fun (x0 y : FMd) (H' : eqFMd x0 y) => @eqFMd_ind (fun x1 y0 : FMd => @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (x1 y0 : Carrier V) (H : @Equal V x1 y0) => @Ap_comp V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f f x1 y0 H (@Refl (MAP V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) f)) (fun (x1 x' y0 y' : FMd) (_ : eqFMd x1 x') (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun x')) (_ : eqFMd y0 y') (H2 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun y')) => @SGROUP_comp (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun x') (FMd_lift_fun y0) (FMd_lift_fun y') H0 H2) (fun x1 y0 z : FMd => @SGROUP_assoc (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z)) (fun x1 : FMd => @MONOID_unit_r (group_monoid (abelian_group_group (@module_carrier R Mod))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @GROUP_comp (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun x1 : FMd => @GROUP_inverse_r (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1)) (fun x1 : FMd => @Refl (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun (x1 y0 z : FMd) (_ : eqFMd x1 y0) (H'1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (_ : eqFMd y0 z) (H'3 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun z)) => @Trans (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z) H'1 H'3) (fun x1 y0 : FMd => @ABELIAN_GROUP_com (@module_carrier R Mod) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) (H : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : eqFMd x1 y0) (H1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @MODULE_comp R Mod a b (FMd_lift_fun x1) (FMd_lift_fun y0) H H1) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @MODULE_dist_r R Mod a b (FMd_lift_fun x1)) (fun (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) => @MODULE_dist_l R Mod a (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (@ring_mult R a b) (FMd_lift_fun x1)) (@module_mult R Mod a (@module_mult R Mod b (FMd_lift_fun x1))) (@MODULE_assoc R Mod a b (FMd_lift_fun x1))) (fun x1 : FMd => @MODULE_unit_l R Mod (FMd_lift_fun x1)) x0 y H')) FMd_var) x) *)
red in |- *.
(* Goal: and (@transitive FMd eqFMd) (@symmetric FMd eqFMd) *)
split; [ try assumption | idtac ].
(* Goal: @reflexive FMd eqFMd *)
(* Goal: @partial_equivalence FMd eqFMd *)
exact eqFMd_refl.
(* Goal: forall x : Carrier V, @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f x) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@comp_hom SET V FMd_set (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@f2 (@G FMd_set Law Unit Inv eqFMd_law eqFMd_law_assoc eqFMd_law0r eqFMd_inv eqFMd_invr) (abelian_group_group (@module_carrier R Mod)) FMd_lift_fun (fun (x0 y : FMd) (H' : eqFMd x0 y) => @eqFMd_ind (fun x1 y0 : FMd => @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (x1 y0 : Carrier V) (H : @Equal V x1 y0) => @Ap_comp V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f f x1 y0 H (@Refl (MAP V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) f)) (fun (x1 x' y0 y' : FMd) (_ : eqFMd x1 x') (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun x')) (_ : eqFMd y0 y') (H2 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun y')) => @SGROUP_comp (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun x') (FMd_lift_fun y0) (FMd_lift_fun y') H0 H2) (fun x1 y0 z : FMd => @SGROUP_assoc (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z)) (fun x1 : FMd => @MONOID_unit_r (group_monoid (abelian_group_group (@module_carrier R Mod))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @GROUP_comp (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun x1 : FMd => @GROUP_inverse_r (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1)) (fun x1 : FMd => @Refl (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun (x1 y0 z : FMd) (_ : eqFMd x1 y0) (H'1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (_ : eqFMd y0 z) (H'3 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun z)) => @Trans (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z) H'1 H'3) (fun x1 y0 : FMd => @ABELIAN_GROUP_com (@module_carrier R Mod) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) (H : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : eqFMd x1 y0) (H1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @MODULE_comp R Mod a b (FMd_lift_fun x1) (FMd_lift_fun y0) H H1) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @MODULE_dist_r R Mod a b (FMd_lift_fun x1)) (fun (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) => @MODULE_dist_l R Mod a (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (@ring_mult R a b) (FMd_lift_fun x1)) (@module_mult R Mod a (@module_mult R Mod b (FMd_lift_fun x1))) (@MODULE_assoc R Mod a b (FMd_lift_fun x1))) (fun x1 : FMd => @MODULE_unit_l R Mod (FMd_lift_fun x1)) x0 y H')) FMd_var) x) *)
red in |- *.
(* Goal: and (@transitive FMd eqFMd) (@symmetric FMd eqFMd) *)
split; [ try assumption | idtac ].
(* Goal: @transitive FMd eqFMd *)
(* Goal: @symmetric FMd eqFMd *)
exact eqFMd_trans.
(* Goal: @symmetric FMd eqFMd *)
exact eqFMd_sym.
Qed.

Definition FMd_set := Build_Setoid eqFMd_Equiv.

Definition FreeModule : MODULE R.
apply
 (BUILD_MODULE (R:=R) (E:=FMd_set) (genlaw:=Law) (e:=Unit) (geninv:=Inv)
    (gen_module_op:=Op)).
(* Goal: forall (x x' y y' : Carrier FMd_set) (_ : @Equal FMd_set x x') (_ : @Equal FMd_set y y'), @Equal FMd_set (Law x y) (Law x' y') *)
(* Goal: forall x y z : Carrier FMd_set, @Equal FMd_set (Law (Law x y) z) (Law x (Law y z)) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Law x Unit) x *)
(* Goal: forall (x y : Carrier FMd_set) (_ : @Equal FMd_set x y), @Equal FMd_set (Inv x) (Inv y) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Law x (Inv x)) Unit *)
(* Goal: forall x y : Carrier FMd_set, @Equal FMd_set (Law x y) (Law y x) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : @Equal FMd_set x y), @Equal FMd_set (Op a x) (Op b y) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) a b) x) (Law (Op a x) (Op b x)) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set), @Equal FMd_set (Op a (Law x y)) (Law (Op a x) (Op a y)) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op a (Op b x)) (Op (@ring_mult R a b) x) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Op (ring_unit R) x) x *)
exact eqFMd_law.
(* Goal: forall x y z : Carrier FMd_set, @Equal FMd_set (Law (Law x y) z) (Law x (Law y z)) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Law x Unit) x *)
(* Goal: forall (x y : Carrier FMd_set) (_ : @Equal FMd_set x y), @Equal FMd_set (Inv x) (Inv y) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Law x (Inv x)) Unit *)
(* Goal: forall x y : Carrier FMd_set, @Equal FMd_set (Law x y) (Law y x) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : @Equal FMd_set x y), @Equal FMd_set (Op a x) (Op b y) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) a b) x) (Law (Op a x) (Op b x)) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set), @Equal FMd_set (Op a (Law x y)) (Law (Op a x) (Op a y)) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op a (Op b x)) (Op (@ring_mult R a b) x) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Op (ring_unit R) x) x *)
exact eqFMd_law_assoc.
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Law x Unit) x *)
(* Goal: forall (x y : Carrier FMd_set) (_ : @Equal FMd_set x y), @Equal FMd_set (Inv x) (Inv y) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Law x (Inv x)) Unit *)
(* Goal: forall x y : Carrier FMd_set, @Equal FMd_set (Law x y) (Law y x) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : @Equal FMd_set x y), @Equal FMd_set (Op a x) (Op b y) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) a b) x) (Law (Op a x) (Op b x)) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set), @Equal FMd_set (Op a (Law x y)) (Law (Op a x) (Op a y)) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op a (Op b x)) (Op (@ring_mult R a b) x) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Op (ring_unit R) x) x *)
exact eqFMd_law0r.
(* Goal: forall (x y : Carrier FMd_set) (_ : @Equal FMd_set x y), @Equal FMd_set (Inv x) (Inv y) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Law x (Inv x)) Unit *)
(* Goal: forall x y : Carrier FMd_set, @Equal FMd_set (Law x y) (Law y x) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : @Equal FMd_set x y), @Equal FMd_set (Op a x) (Op b y) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) a b) x) (Law (Op a x) (Op b x)) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set), @Equal FMd_set (Op a (Law x y)) (Law (Op a x) (Op a y)) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op a (Op b x)) (Op (@ring_mult R a b) x) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Op (ring_unit R) x) x *)
exact eqFMd_inv.
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Law x (Inv x)) Unit *)
(* Goal: forall x y : Carrier FMd_set, @Equal FMd_set (Law x y) (Law y x) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : @Equal FMd_set x y), @Equal FMd_set (Op a x) (Op b y) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) a b) x) (Law (Op a x) (Op b x)) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set), @Equal FMd_set (Op a (Law x y)) (Law (Op a x) (Op a y)) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op a (Op b x)) (Op (@ring_mult R a b) x) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Op (ring_unit R) x) x *)
exact eqFMd_invr.
(* Goal: forall x y : Carrier FMd_set, @Equal FMd_set (Law x y) (Law y x) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : @Equal FMd_set x y), @Equal FMd_set (Op a x) (Op b y) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) a b) x) (Law (Op a x) (Op b x)) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set), @Equal FMd_set (Op a (Law x y)) (Law (Op a x) (Op a y)) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op a (Op b x)) (Op (@ring_mult R a b) x) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Op (ring_unit R) x) x *)
exact eqFMd_com.
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : @Equal FMd_set x y), @Equal FMd_set (Op a x) (Op b y) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) a b) x) (Law (Op a x) (Op b x)) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set), @Equal FMd_set (Op a (Law x y)) (Law (Op a x) (Op a y)) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op a (Op b x)) (Op (@ring_mult R a b) x) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Op (ring_unit R) x) x *)
exact eqFMd_op_comp.
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) a b) x) (Law (Op a x) (Op b x)) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set), @Equal FMd_set (Op a (Law x y)) (Law (Op a x) (Op a y)) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op a (Op b x)) (Op (@ring_mult R a b) x) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Op (ring_unit R) x) x *)
exact eqFMd_oplin_l.
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier FMd_set), @Equal FMd_set (Op a (Law x y)) (Law (Op a x) (Op a y)) *)
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op a (Op b x)) (Op (@ring_mult R a b) x) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Op (ring_unit R) x) x *)
exact eqFMd_oplin_r.
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier FMd_set), @Equal FMd_set (Op a (Op b x)) (Op (@ring_mult R a b) x) *)
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Op (ring_unit R) x) x *)
exact eqFMd_op_assoc.
(* Goal: forall x : Carrier FMd_set, @Equal FMd_set (Op (ring_unit R) x) x *)
exact eqFMd_op_unit.
Defined.
Section Universal_prop.
Variable Mod : MODULE R.
Variable f : Hom V Mod.

Fixpoint FMd_lift_fun (p : FreeModule) : Mod :=
  match p with
  | Var v => f v
  | Law p1 p2 => sgroup_law Mod (FMd_lift_fun p1) (FMd_lift_fun p2)
  | Unit => monoid_unit Mod
  | Inv p1 => group_inverse Mod (FMd_lift_fun p1)
  | Op a p1 => module_mult a (FMd_lift_fun p1)
  end.

Definition FMd_lift : Hom FreeModule Mod.
apply
 (BUILD_HOM_MODULE (R:=R) (Mod:=FreeModule) (Mod':=Mod) (ff:=FMd_lift_fun)).
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule))))) x y), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x) (FMd_lift_fun y) *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))) x y)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x) (FMd_lift_fun y)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R FreeModule)))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (@module_mult R FreeModule a x)) (@module_mult R Mod a (FMd_lift_fun x)) *)
intros x y H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x) (FMd_lift_fun y) *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))) x y)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x) (FMd_lift_fun y)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R FreeModule)))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (@module_mult R FreeModule a x)) (@module_mult R Mod a (FMd_lift_fun x)) *)
elim H'; simpl in |- *; auto with algebra.
(* Goal: forall (x y z : FMd) (_ : eqFMd x y) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x) (FMd_lift_fun y)) (_ : eqFMd y z) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y) (FMd_lift_fun z)), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x) (FMd_lift_fun z) *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))) x y)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x) (FMd_lift_fun y)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R FreeModule)))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (@module_mult R FreeModule a x)) (@module_mult R Mod a (FMd_lift_fun x)) *)
intros x0 y0 z H'0 H'1 H'2 H'3; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x0) (FMd_lift_fun z) *)
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))) x y)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x) (FMd_lift_fun y)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R FreeModule)))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun (@module_mult R FreeModule a x)) (@module_mult R Mod a (FMd_lift_fun x)) *)
apply Trans with (FMd_lift_fun y0); auto with algebra.
(* Goal: forall (x y : Carrier V) (_ : @Equal V x y), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule))))) (Var x) (Var y) *)
simpl in |- *; auto with algebra.
(* Goal: forall (x y : Carrier V) (_ : @Equal V x y), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule))))) (Var x) (Var y) *)
simpl in |- *; auto with algebra.
(* Goal: forall (x y : Carrier V) (_ : @Equal V x y), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule))))) (Var x) (Var y) *)
simpl in |- *; auto with algebra.
Defined.

Definition FMd_var : Hom V FreeModule.
(* Goal: Carrier (@Hom SET V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule)))))) *)
apply (Build_Map (A:=V) (B:=FreeModule) (Ap:=Var)).
(* Goal: forall x : Carrier V, @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f x) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@comp_hom SET V FMd_set (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@f2 (@G FMd_set Law Unit Inv eqFMd_law eqFMd_law_assoc eqFMd_law0r eqFMd_inv eqFMd_invr) (abelian_group_group (@module_carrier R Mod)) FMd_lift_fun (fun (x0 y : FMd) (H' : eqFMd x0 y) => @eqFMd_ind (fun x1 y0 : FMd => @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (x1 y0 : Carrier V) (H : @Equal V x1 y0) => @Ap_comp V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f f x1 y0 H (@Refl (MAP V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) f)) (fun (x1 x' y0 y' : FMd) (_ : eqFMd x1 x') (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun x')) (_ : eqFMd y0 y') (H2 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun y')) => @SGROUP_comp (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun x') (FMd_lift_fun y0) (FMd_lift_fun y') H0 H2) (fun x1 y0 z : FMd => @SGROUP_assoc (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z)) (fun x1 : FMd => @MONOID_unit_r (group_monoid (abelian_group_group (@module_carrier R Mod))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @GROUP_comp (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun x1 : FMd => @GROUP_inverse_r (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1)) (fun x1 : FMd => @Refl (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun (x1 y0 z : FMd) (_ : eqFMd x1 y0) (H'1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (_ : eqFMd y0 z) (H'3 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun z)) => @Trans (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z) H'1 H'3) (fun x1 y0 : FMd => @ABELIAN_GROUP_com (@module_carrier R Mod) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) (H : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : eqFMd x1 y0) (H1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @MODULE_comp R Mod a b (FMd_lift_fun x1) (FMd_lift_fun y0) H H1) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @MODULE_dist_r R Mod a b (FMd_lift_fun x1)) (fun (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) => @MODULE_dist_l R Mod a (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (@ring_mult R a b) (FMd_lift_fun x1)) (@module_mult R Mod a (@module_mult R Mod b (FMd_lift_fun x1))) (@MODULE_assoc R Mod a b (FMd_lift_fun x1))) (fun x1 : FMd => @MODULE_unit_l R Mod (FMd_lift_fun x1)) x0 y H')) FMd_var) x) *)
red in |- *.
(* Goal: forall (x y : Carrier V) (_ : @Equal V x y), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R FreeModule))))) (Var x) (Var y) *)
simpl in |- *; auto with algebra.
Defined.

Lemma FMd_comp_prop :
 Equal f (comp_hom (FMd_lift:Hom (FreeModule:SET) Mod) FMd_var).
(* Goal: forall x : Carrier V, (let (Carrier, Equal, _) as s return (relation (Carrier s)) := sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) in Equal) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f x) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@comp_hom SET V FMd_set (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@f2 (@G FMd_set Law Unit Inv eqFMd_law eqFMd_law_assoc eqFMd_law0r eqFMd_inv eqFMd_invr) (abelian_group_group (@module_carrier R Mod)) FMd_lift_fun (fun (x0 y : FMd) (H' : eqFMd x0 y) => @eqFMd_ind (fun x1 y0 : FMd => @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (x1 y0 : Carrier V) (H : @Equal V x1 y0) => @Ap_comp V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f f x1 y0 H (@Refl (MAP V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) f)) (fun (x1 x' y0 y' : FMd) (_ : eqFMd x1 x') (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun x')) (_ : eqFMd y0 y') (H2 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun y')) => @SGROUP_comp (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun x') (FMd_lift_fun y0) (FMd_lift_fun y') H0 H2) (fun x1 y0 z : FMd => @SGROUP_assoc (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z)) (fun x1 : FMd => @MONOID_unit_r (group_monoid (abelian_group_group (@module_carrier R Mod))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @GROUP_comp (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun x1 : FMd => @GROUP_inverse_r (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1)) (fun x1 : FMd => @Refl (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun (x1 y0 z : FMd) (_ : eqFMd x1 y0) (H'1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (_ : eqFMd y0 z) (H'3 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun z)) => @Trans (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z) H'1 H'3) (fun x1 y0 : FMd => @ABELIAN_GROUP_com (@module_carrier R Mod) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) (H : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : eqFMd x1 y0) (H1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @MODULE_comp R Mod a b (FMd_lift_fun x1) (FMd_lift_fun y0) H H1) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @MODULE_dist_r R Mod a b (FMd_lift_fun x1)) (fun (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) => @MODULE_dist_l R Mod a (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (@ring_mult R a b) (FMd_lift_fun x1)) (@module_mult R Mod a (@module_mult R Mod b (FMd_lift_fun x1))) (@MODULE_assoc R Mod a b (FMd_lift_fun x1))) (fun x1 : FMd => @MODULE_unit_l R Mod (FMd_lift_fun x1)) x0 y H')) FMd_var) x) *)
simpl in |- *.
(* Goal: forall x : Carrier V, @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f x) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@comp_hom SET V FMd_set (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@f2 (@G FMd_set Law Unit Inv eqFMd_law eqFMd_law_assoc eqFMd_law0r eqFMd_inv eqFMd_invr) (abelian_group_group (@module_carrier R Mod)) FMd_lift_fun (fun (x0 y : FMd) (H' : eqFMd x0 y) => @eqFMd_ind (fun x1 y0 : FMd => @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (x1 y0 : Carrier V) (H : @Equal V x1 y0) => @Ap_comp V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f f x1 y0 H (@Refl (MAP V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) f)) (fun (x1 x' y0 y' : FMd) (_ : eqFMd x1 x') (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun x')) (_ : eqFMd y0 y') (H2 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun y')) => @SGROUP_comp (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun x') (FMd_lift_fun y0) (FMd_lift_fun y') H0 H2) (fun x1 y0 z : FMd => @SGROUP_assoc (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z)) (fun x1 : FMd => @MONOID_unit_r (group_monoid (abelian_group_group (@module_carrier R Mod))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @GROUP_comp (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun x1 : FMd => @GROUP_inverse_r (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1)) (fun x1 : FMd => @Refl (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun (x1 y0 z : FMd) (_ : eqFMd x1 y0) (H'1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (_ : eqFMd y0 z) (H'3 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun z)) => @Trans (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z) H'1 H'3) (fun x1 y0 : FMd => @ABELIAN_GROUP_com (@module_carrier R Mod) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) (H : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : eqFMd x1 y0) (H1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @MODULE_comp R Mod a b (FMd_lift_fun x1) (FMd_lift_fun y0) H H1) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @MODULE_dist_r R Mod a b (FMd_lift_fun x1)) (fun (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) => @MODULE_dist_l R Mod a (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (@ring_mult R a b) (FMd_lift_fun x1)) (@module_mult R Mod a (@module_mult R Mod b (FMd_lift_fun x1))) (@MODULE_assoc R Mod a b (FMd_lift_fun x1))) (fun x1 : FMd => @MODULE_unit_l R Mod (FMd_lift_fun x1)) x0 y H')) FMd_var) x) *)
red in |- *.
(* Goal: forall x : Carrier V, @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f x) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@comp_hom SET V FMd_set (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@f2 (@G FMd_set Law Unit Inv eqFMd_law eqFMd_law_assoc eqFMd_law0r eqFMd_inv eqFMd_invr) (abelian_group_group (@module_carrier R Mod)) FMd_lift_fun (fun (x0 y : FMd) (H' : eqFMd x0 y) => @eqFMd_ind (fun x1 y0 : FMd => @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (x1 y0 : Carrier V) (H : @Equal V x1 y0) => @Ap_comp V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f f x1 y0 H (@Refl (MAP V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) f)) (fun (x1 x' y0 y' : FMd) (_ : eqFMd x1 x') (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun x')) (_ : eqFMd y0 y') (H2 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun y')) => @SGROUP_comp (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun x') (FMd_lift_fun y0) (FMd_lift_fun y') H0 H2) (fun x1 y0 z : FMd => @SGROUP_assoc (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z)) (fun x1 : FMd => @MONOID_unit_r (group_monoid (abelian_group_group (@module_carrier R Mod))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @GROUP_comp (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun x1 : FMd => @GROUP_inverse_r (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1)) (fun x1 : FMd => @Refl (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun (x1 y0 z : FMd) (_ : eqFMd x1 y0) (H'1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (_ : eqFMd y0 z) (H'3 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun z)) => @Trans (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z) H'1 H'3) (fun x1 y0 : FMd => @ABELIAN_GROUP_com (@module_carrier R Mod) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) (H : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : eqFMd x1 y0) (H1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @MODULE_comp R Mod a b (FMd_lift_fun x1) (FMd_lift_fun y0) H H1) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @MODULE_dist_r R Mod a b (FMd_lift_fun x1)) (fun (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) => @MODULE_dist_l R Mod a (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (@ring_mult R a b) (FMd_lift_fun x1)) (@module_mult R Mod a (@module_mult R Mod b (FMd_lift_fun x1))) (@MODULE_assoc R Mod a b (FMd_lift_fun x1))) (fun x1 : FMd => @MODULE_unit_l R Mod (FMd_lift_fun x1)) x0 y H')) FMd_var) x) *)
red in |- *.
(* Goal: forall x : Carrier V, (let (Carrier, Equal, _) as s return (relation (Carrier s)) := sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) in Equal) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f x) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@comp_hom SET V FMd_set (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@f2 (@G FMd_set Law Unit Inv eqFMd_law eqFMd_law_assoc eqFMd_law0r eqFMd_inv eqFMd_invr) (abelian_group_group (@module_carrier R Mod)) FMd_lift_fun (fun (x0 y : FMd) (H' : eqFMd x0 y) => @eqFMd_ind (fun x1 y0 : FMd => @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (x1 y0 : Carrier V) (H : @Equal V x1 y0) => @Ap_comp V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f f x1 y0 H (@Refl (MAP V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) f)) (fun (x1 x' y0 y' : FMd) (_ : eqFMd x1 x') (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun x')) (_ : eqFMd y0 y') (H2 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun y')) => @SGROUP_comp (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun x') (FMd_lift_fun y0) (FMd_lift_fun y') H0 H2) (fun x1 y0 z : FMd => @SGROUP_assoc (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z)) (fun x1 : FMd => @MONOID_unit_r (group_monoid (abelian_group_group (@module_carrier R Mod))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @GROUP_comp (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun x1 : FMd => @GROUP_inverse_r (abelian_group_group (@module_carrier R Mod)) (FMd_lift_fun x1)) (fun x1 : FMd => @Refl (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1)) (fun (x1 y0 : FMd) (_ : eqFMd x1 y0) (H0 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) H0) (fun (x1 y0 z : FMd) (_ : eqFMd x1 y0) (H'1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) (_ : eqFMd y0 z) (H'3 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun y0) (FMd_lift_fun z)) => @Trans (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0) (FMd_lift_fun z) H'1 H'3) (fun x1 y0 : FMd => @ABELIAN_GROUP_com (@module_carrier R Mod) (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) (H : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : eqFMd x1 y0) (H1 : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (FMd_lift_fun x1) (FMd_lift_fun y0)) => @MODULE_comp R Mod a b (FMd_lift_fun x1) (FMd_lift_fun y0) H H1) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @MODULE_dist_r R Mod a b (FMd_lift_fun x1)) (fun (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 y0 : FMd) => @MODULE_dist_l R Mod a (FMd_lift_fun x1) (FMd_lift_fun y0)) (fun (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x1 : FMd) => @Sym (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (@ring_mult R a b) (FMd_lift_fun x1)) (@module_mult R Mod a (@module_mult R Mod b (FMd_lift_fun x1))) (@MODULE_assoc R Mod a b (FMd_lift_fun x1))) (fun x1 : FMd => @MODULE_unit_l R Mod (FMd_lift_fun x1)) x0 y H')) FMd_var) x) *)
simpl in |- *.
(* Goal: forall x : Carrier V, (let (Carrier, Equal, _) as s return (relation (Carrier s)) := sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) in Equal) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f x) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f x) *)
intros x; try assumption.
(* Goal: (let (Carrier, Equal, _) as s return (relation (Carrier s)) := sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) in Equal) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f x) (@Ap V (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) f x) *)
exact (Refl (f x)).
Qed.
End Universal_prop.
End Free_Module_def.
Hint Resolve FMd_comp_prop: algebra.
