proposition: Lemma pointwise_relation_is_guarded_pointwise_relation: forall {A B : Type} (R : relation B), same_relation _ (pointwise_relation A R) (guarded_pointwise_relation (fun _ => True) R).
proof: Proof. intros. rewrite same_relation_spec. hnf; intros. hnf; intros. rewrite guarded_pointwise_relation_spec. unfold pointwise_relation. firstorder. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.Relation_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext