(*** H_coafter_fwd_isid2 *)
definition H_gr_coafter_des_ist_sn_isi: predicate gr_map ≝
λf1. ∀f2,f. f1 ~⊚ f2 ≘ f → 𝐓❪f1❫ → 𝐈❪f❫ → 𝐈❪f2❫.
(*** H_coafter_fwd_isid2 *)
definition H_gr_coafter_des_ist_sn_isi: predicate gr_map ≝
λf1. ∀f2,f. f1 ~⊚ f2 ≘ f → 𝐓❪f1❫ → 𝐈❪f❫ → 𝐈❪f2❫.