proposition: Lemma nf_proof_unicity : forall (alpha:T1) (H H': nf alpha), H = H'.
proof: Proof. intros; red in H, H'; apply eq_proofs_unicity_on; decide equality. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)