proposition: Lemma replace_ioE vT eT1 eT2 st1 st2 lv1 lv2 le1 le2 i o H e : admissible_l e -> @replace_ioL (point (@Graph _ _ vT eT1 st1 lv1 le1) i o) (point (@Graph _ _ vT eT2 st2 lv2 le2) i o) H e = e.
proof: Proof. elim: e => //=. case => [[a|a] [b|b]] l /= IH. all: rewrite /admissible_l /=. all: first [case/and3P|case/andP|idtac]. all: repeat (case/set2P => ->). all: move => HA; rewrite ?IH ?eqxx //. all: by case: (altP (i =P o)) => [->|?]. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)