Documentation

Foundation.FirstOrder.Arith.StrictHierarchy

Instances For
    theorem LO.FirstOrder.Arith.StrictHierarchy.rew {L : LO.FirstOrder.Language} [L.LT] {μ₁ : Type u_1} {n₁ : } {Γ : LO.Polarity} {s : } {μ₂ : Type u_2} {n₂ : } {p : LO.FirstOrder.Semiformula L μ₁ n₁} (h : LO.FirstOrder.Arith.StrictHierarchy Γ s p) (ω : LO.FirstOrder.Rew L μ₁ n₁ μ₂ n₂) :
    theorem LO.FirstOrder.Arith.StrictHierarchy.rew_iff {L : LO.FirstOrder.Language} [L.LT] {μ₁ : Type u_1} {n₁ : } {μ₂ : Type u_2} {n₂ : } {Γ : LO.Polarity} {s : } {p : LO.FirstOrder.Semiformula L μ₁ n₁} (ω : LO.FirstOrder.Rew L μ₁ n₁ μ₂ n₂) :