proposition: Lemma uniq_labels_build_tree_rec h s k i : uniq_path (tanner_rel H) (id_of_kind k i) s -> uniq (labels (build_tree_rec H rW h s k i)).
proof: Proof. elim: h s k i => [|h Hh] s k i Hi //=. rewrite -map_comp. set labels_tree := labels \o _. case Ha: (id_of_kind k i \in _) => /=. move/flattenP: Ha => [l] /mapP [j Hj ->{l}] Hil. rewrite select_children_spec in Hj. case/labels_build_tree_rec: Hil => [|p [/andP[_ /=]]]. rewrite /uniq_path /= sym_tanner_rel. by case/andP: Hj Hi => -> -> /andP /=[-> ->]. by rewrite mem_cat in_cons eqxx orbT. set l := select_children H s k i in Ha *. have Hch: uniq l by apply select_children_uniq. have Hsub: {subset l <= select_children H s k i} by []. elim: l => //= c l IH in Ha Hch Hsub *. rewrite cat_uniq. have Hspec: c \in select_children H s k i. by apply Hsub; rewrite in_cons eqxx. rewrite select_children_spec in Hspec. apply/andP; split. apply Hh. rewrite /uniq_path /= sym_tanner_rel. by case/andP: Hspec Hi => -> -> /andP /=[-> ->]. rewrite {}IH ?andbT; first last. by move=> x Hx; apply Hsub; rewrite in_cons Hx orbT. by move/andP/proj2: Hch. move: Ha; rewrite mem_cat. by case Hl: (_ \in labels _). apply/hasP => /= -[x Hx Hmem] {Ha Hh}. case/labels_build_tree_rec: Hmem => [|p [Hun [Hl _]]]. rewrite /uniq_path /= sym_tanner_rel. by case/andP: Hspec Hi => -> -> /andP /=[-> ->]. move/flattenP: Hx => /= [d /mapP[y Hy ->{d}] Hxd]. have Hspec': y \in c :: l by rewrite in_cons Hy orbT. apply Hsub in Hspec'. rewrite {Hsub Hspec} select_children_spec in Hspec'. case/labels_build_tree_rec: Hxd => [|p' [Hun' [Hl' _]]]. rewrite /uniq_path /= sym_tanner_rel. by case/andP: Hspec' Hi => -> -> /andP /=[-> ->]. move: (@tanner_acyclic (id_of_kind k i) (id_of_kind (negk k) y) (rev (belast x p') ++ p)) {Hspec' Hi}. rewrite in_cons mem_cat /=. rewrite id_of_kind_neq /=. move/andP/proj2: (Hun'). rewrite -cat1s catA cat_uniq mem_rev. move/andP/proj2/andP/proj1/norP/proj1. case Hip': (_ \in belast x p') => /=. by rewrite (mem_belast Hip'). move => _. move/andP/proj2: (Hun). rewrite /= cat_uniq /= sym_tanner_rel. move/and4P => [_ _] /norP/proj1 Hid _ /(_ Hid){Hid}. case Hiy: (tanner_rel H _ _); last first. move=> _; move/andP/proj1: Hun' Hiy. rewrite -cat_rcons cat_path => /andP/proj1. destruct p'; simpl in Hl'. by rewrite /= Hl' andbT => ->. by rewrite lastI Hl' /= rcons_path !last_rcons => /andP/proj2 ->. rewrite /= rcons_cat cat_path. move/andP/proj1: Hun'. rewrite cat_path => /andP/proj1 Hun'. rewrite (eq_path (sym_tanner_rel H)) -rev_path in Hun'. rewrite -Hl' Hun' /=. move/andP/proj1: Hun. rewrite -cat_rcons cat_path => /andP/proj1 Hun. destruct p' as [|z p']; simpl in *. rewrite Hun Hl Hl'. rewrite (inj_eq (@id_of_kind_inj _)). move/(_ (eqxx true)) => Hcy. by rewrite (eqP Hcy) Hy in Hch. rewrite rev_cons last_rcons Hun. rewrite last_cat last_rcons. rewrite Hl Hl' (inj_eq (@id_of_kind_inj _)). move/(_ (eqxx true)) => Hcy. by rewrite (eqP Hcy) Hy in Hch. Qed.
imports: Wf_nat Init.Wf Recdef Reals mathcomp(all_ssreflect perm zmodp matrix ssralg) mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2 fdist channel pproba linearcode subgraph_partition tanner tanner_partition summary ldpc checksum ldpc_algo