have h : ∀ x, Q x :=
by
  intros x
  apply normalizing_ind R
  . intros x ih'
    constructor
    . apply ih
      intros y red_x_y
      cases red_x_y
      . apply (ih' _ _).1; trivial
      . apply (ih' _ _).2 <;> trivial
    . intros y red_x_y
      cases red_x_y
      . apply (ih' _ _).1; trivial
      . apply (ih' _ _).2 <;> trivial
  . 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), P x
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
h : ∀ (x : A), Q x
⊢ ∀ (x : A), P x