proposition: Lemma nf_proof_unicity : forall (alpha:t) (H H': nf alpha), H = H'.
proof: Proof. intros; red in H, H'; apply eq_proofs_unicity_on; decide equality. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )