proposition: Lemma nf_inv3 : forall i n j n' b', nf (cons i n (cons j n' b')) -> Nat.lt j i.
proof: Proof. unfold nf; cbn; destruct b'; try discriminate; auto with T1; intro H; red in H; repeat rewrite andb_true_iff in H. - destruct H as [_ H]; destruct i. + discriminate. + rewrite Nat.leb_le in H; lia. - destruct p; destruct i. + destruct j; destruct H; discriminate. + destruct H; rewrite Nat.leb_le in H0; lia. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )