proposition: Lemma iso_eq_F0_F1 : forall r s : {perm cube}, r \in dir_iso3 -> s \in dir_iso3 -> r F0 = s F0 -> r F1 = s F1 -> r = s.
proof: Proof. move=> r s; rewrite !L_iso => hr hs hrs0 hrs1; apply: sop_inj; apply/eqP. move/eqP: hrs0; apply/implyP; move/eqP: hrs1; apply/implyP; rewrite -!sop_spec. by move/sop: r hr; apply/allP; move/sop: s hs; apply/allP; vm_compute. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset fingroup) mathcomp(action perm primitive_action)