intros norm
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ normalizing R → normalizing fun x x_1 => trans_clos R x x_1
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
⊢ normalizing fun x x_1 => trans_clos R x x_1