proposition: Lemma neig4boxE : relpre val (grel neig4) =2 grel (fun b : box => pmap insub (neig4 b)).
proof: Proof. by move=> b1 b2 /=; rewrite mem_pmap_sub. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition