proposition: Lemma cons_nf : forall i n j n' b, Nat.lt j i -> nf(cons j n' b)-> nf(cons i n (cons j n' b)).
proof: Proof. unfold nf; simpl; intros i n j n' b' Hltji Ha. apply Nat.ltb_lt in Hltji as ->. destruct b'; auto with bool. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )