proposition: Lemma OO_eq_intro : forall alpha beta : OO, data alpha = data beta -> alpha = beta.
proof: Proof. destruct alpha, beta; simpl; intros; subst; f_equal; auto; apply nf_proof_unicity. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )