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