proposition: Lemma admissible_map : map_pairs sumA (map_pairs (sumf id sumC) (map_pairs sumA' l)) = map_pairs inl (replace_ioL l).
proof: Proof. rewrite 2!map_map_pairs. induction l as [|[a1 a2] q IH]=>//. simpl. move: A =>/andP[/=A1 /andP[/=A2 Q]]. f_equal. f_equal. destruct a1 as [[x|[]]|x]=>//=. case/set2P : A1 => [] [->]; rewrite sum_eqE ?eqxx //. by case: (altP (input =P output)) => [->|]. exfalso. clear -A1. by rewrite !inE in A1. destruct a2 as [[x|[]]|x]=>//=. case/set2P : A2 => [] [->]; rewrite sum_eqE ?eqxx //. by case: (altP (input =P output)) => [->|]. exfalso. clear -A2. by rewrite !inE in A2. apply IH, Q. 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)