Research proof index

A monotone predicate P is objective if its value does not depend on the index: P i ⊢ P j for all i j. Equivalently P ⊣⊢ <obj> P. -/ @[rocq_alias Objective] class Objective {I : BiIndex} {PROP : Type _} [BI PROP] (P : MonPred I PROP) : Prop where objective_at : ∀ i j : I.car, P.monPred_at i ⊢ P.monPred_at j namespace MonPred variable {I : BiIndex...