proposition: Lemma shell_injective (V V' : P_ n (A , B)) (Vctyp : V \in \nu^{B}(P)) ta (Hta : ta \in T_{P}) : V.-shell ta = V'.-shell ta -> forall a b, (JType.f V) a b = (JType.f V') a b.
proof: Proof. move=> H a b. rewrite /cond_type in_set in Vctyp. move/forallP in Vctyp. move: {Vctyp}(Vctyp ta) => Vctyp. move/implyP in Vctyp. move: {Vctyp}(Vctyp Hta) => Vctyp. case/set0Pn : Vctyp => tb V_tb. have V'_tb : tb \in V'.-shell ta by rewrite -H. apply val_inj => /=. move: V_tb; rewrite in_set => /forallP/(_ a)/forallP/(_ b)/eqP => <-. move: V'_tb; by rewrite in_set => /forallP/(_ a)/forallP/(_ b)/eqP => <-. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types