(*** H_coafter_inj *)
definition H_gr_coafter_inj: predicate gr_map ≝
λf1. 𝐓❪f1❫ →
∀f,f21,f22. f1 ~⊚ f21 ≘ f → f1 ~⊚ f22 ≘ f → f21 ≡ f22.
(*** H_coafter_inj *)
definition H_gr_coafter_inj: predicate gr_map ≝
λf1. 𝐓❪f1❫ →
∀f,f21,f22. f1 ~⊚ f21 ≘ f → f1 ~⊚ f22 ≘ f → f21 ≡ f22.