proposition: Lemma HCompACA : (t' \h s') \v (t \h s) = (t' \v t) \h (s' \v s).
proof: Proof. apply nattrans_ext => c /=. rewrite !HCompE !VCompE -compA -[in RHS]compA; congr (_ \o _). by rewrite natural_head -functor_o. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)