proposition: Lemma nf_ref: forall a, T1.nf (refine a) <-> nf a.
proof: Proof. induction a. - cbn; split; trivial. - destruct a as [i n]; split. + intro H; destruct a0. * apply single_nf. * destruct p. apply cons_nf. -- cbn in H; apply T1.nf_inv3 in H; now apply T1.lt_fin_iff. -- cbn in H; apply IHa; apply T1.nf_inv2 in H; apply H. + intro H; destruct a0. * apply T1.single_nf, T1.nf_fin. * destruct p; cbn; apply T1.cons_nf. -- apply nf_inv3 in H; now apply T1.lt_fin_iff. -- apply T1.nf_fin. -- apply nf_inv2 in H; now rewrite IHa. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )