proposition: Lemma Gmorph_intersect : forall x y, GoM (mat_andb M N) x y <-> GoM M x y /\ GoM N x y.
proof: Proof. intros; unfold GoM. rewrite andb_mat_unbound. destruct (M [[x, y]]); destruct (M [[x, y]]); intuition; simpl. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)