proposition: Lemma nf_inv2 : forall i n b, nf (cons i n b) -> nf b.
proof: Proof. unfold nf; cbn; destruct i, b; auto. destruct p; cbn; destruct b. - auto with bool. - destruct p; auto with bool. rewrite andb_false_r; discriminate. - destruct p; intro H; apply andb_prop in H; now destruct H. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )