proposition: Lemma nf_fin i : nf (fin i).
proof: Proof. destruct i. - auto with T2. - constructor 2; auto with T2. Qed.
imports: Coq(Arith Compare_dec Relations Wellfounded Lia) hydras(More_Arith Restriction T1 OrdNotations Compat815)