proposition: Theorem inject_injective (beta gamma : T1) : nf beta -> nf gamma -> inject beta = inject gamma -> beta = gamma.
proof: Proof. intros H H0 H1. destruct (LT_eq_LT_dec H H0) as [[H2 | H2] | H2]; auto. destruct H2 as [H3 [H4 H5]]. apply inject_mono in H4; auto. rewrite H1 in H4; auto. destruct (lt_irrefl H4); auto. destruct H2 as [H3 [H4 H5]]. apply inject_mono in H4; auto. rewrite H1 in H4; auto. destruct (lt_irrefl H4); auto. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)