proposition: Lemma isprogressive_idfun {P : Poset} : isprogressive (idfun P).
proof: Proof. intro; apply isrefl_posetRelation. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.WellOrderedSets UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo