proposition: Lemma eq_alpha_beta {A : eqType} F {k} (t1 t2 : tag k) (l1 l2 : list A) : t1 = t2 -> perm_eq l1 l2 -> alpha_beta t1 (map F l1) = alpha_beta t2 (map F l2).
proof: Proof. move=> Ht ?; rewrite /alpha_beta; case: t1 t2 Ht => [|v] t2 <-. - rewrite !alpha_map; exact/perm_big. - rewrite !beta_map; congr beta_op; exact/perm_big. 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