proposition: Lemma diagonal_prop_PER {A : Type} (P : A -> Prop) : PER (diagonal_prop P).
proof: Proof. constructor. red. intros. cbn in *. unfold diagonal_prop in *; tauto. red. intros. cbn in *. unfold diagonal_prop in *; tauto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)