proposition: Lemma UA_FM_law1 : UA_law1 UA_FM_mor UA_FM_diese.
proof: Proof. unfold UA_law1, UA_eq in |- *; intros B f. unfold UA_FM_mor in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. intro a; apply Midr1. Qed.
imports: FunForget FreeMonoid UniversalArrow