proposition: Lemma m_nf : forall h, nf (m h).
proof: Proof. induction h using Hydra_rect2 with (P0 := fun s => nf (ms s)). - destruct h; simpl; auto. - constructor. - intros; rewrite ms_eqn2; apply oplus_nf. + now apply nf_phi0. + assumption. Qed.
imports: hydras(E0 Hessenberg)