proposition: Lemma partial_graph_incl: forall (t g: UAdjMatGG), is_partial_graph t g -> incl (EList t) (EList g).
proof: Proof. unfold incl; intros. rewrite EList_evalid in *. apply H; auto. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.find_lemmas CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.undirected_graph CertiGraph.graph.MathAdjMatGraph