proposition: Lemma Included_Full_set: forall A P, Included A P (Full_set A).
proof: Proof. intros. hnf; unfold In; intros. apply Full_set_spec; auto. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Equivalence Coq.Sets.Ensembles Coq.Sets.Constructive_sets CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext