proposition: Lemma oiso2_input (F G : pre_graph) (i : F ⩭2 G) : i (p_in F) = p_in G.
proof: Proof. case: i => isF isG i /=. rewrite vfun_bodyE => [|p]. exact: p_inP. rewrite [Sub _ _](_ : _ = @input _ _ (pack F)) ?iso2_input //. exact: val_inj. Qed.
imports: Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(rewriting open_confluence finmap_plus)