proposition: Lemma tag_eqP k : Equality.axiom (@tag_eq_bool k).
proof: Proof. move=> [|r] y; refine (match y with Func => _ | Var r' => _ end) => //=. by constructor. case Hrr': (r == r'). by rewrite (eqP Hrr'); constructor. constructor. move=> Hv. move: Hrr'. by injection Hv; move=> ->; rewrite eqxx. 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