. trivial
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ normalizing R
no goals