proposition: Lemma dest_ports_seqs_step c l : dest_ports_seqs c l.+1 = \bigcup_(t in dest_ports c #|border (nodes c)|) cons_tuple (tuple_to_partial (def_port, set0) t) @: dest_ports_seqs (switch (step_it c t)) l.
proof: Proof. rewrite -curry_imset2l_dep. symmetry. apply/setP => /= t. apply/imset2P. case: ifP => /= Ht. - destruct t as [x Hszx]. destruct x as [|x s] => //. have Hs := Hszx; rewrite eqSS in Hs. move: Ht. rewrite inE /= => /andP[Hout] /and4P[Hall Hun Htriv Hcp]. exists (partial_to_tuple (border (nodes c)) x) (Tuple Hs). rewrite inE /partial_to_tuple /=. by rewrite Hun Hall Htriv. by rewrite inE. rewrite partial_to_tupleK //. by apply/val_inj. - move=> [/= x t' Hx Ht' Htt']. move/negP: Ht; apply. subst t. move: Ht'. destruct t' as [t Ht] => /=. rewrite inE /= inE => Hck. move: Hx. rewrite inE => /and3P[Hall Hun Htriv]. rewrite /= tuple_to_partial_out /=. by rewrite tuple_to_partial_enumK Hall Hun Htriv Hck. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner