proposition: Lemma hb_strip_conjE inner outer : is_part inner -> is_part outer -> hb_strip (conj_part inner) (conj_part outer) = vb_strip inner outer.
proof: Proof. Proof using. move=> Hinn Hout; apply/idP/idP; last exact: vb_strip_conj. rewrite -{2}(conj_partK Hinn) -{2}(conj_partK Hout). exact: hb_strip_conj (is_part_conj Hinn) (is_part_conj Hout). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition