proposition: Lemma HComp_VH_aux : t \h s = (NId G' \h s) \v (t \h NId F).
proof: Proof. by apply nattrans_ext=> a; rewrite VCompE HCompE HIdComp HCompId -natural. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)