proposition: Theorem h2o_nf : forall h, nf (h2o h).
proof: Proof. intro h; elim h using Hydra_rect2 with (P0 := fun hs => nfs (h2ol hs)). simpl. constructor. simpl. intros. apply sort_nf. auto. intros;apply nf_to_nfs. simpl. constructor. auto. simpl;auto. constructor;auto. Qed.
imports: Arith Omega List EPSILON0 MSE0