simplify.apply not_eq_OZ_pos.
simplify.apply not_eq_OZ_neg.
elim y.
- simplify.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.
+ simplify.unfold Not.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.
simplify.apply eqb_elim.
intro.simplify.apply eq_f.assumption.
- intro.simplify.intro.apply H.apply inj_pos.assumption.
+ intro.simplify.unfold Not.intro.apply H.apply inj_pos.assumption.
simplify.apply not_eq_pos_neg.
elim y.
- simplify.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
- simplify.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
+ simplify.unfold Not.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
+ simplify.unfold Not.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
simplify.apply eqb_elim.
intro.simplify.apply eq_f.assumption.
- intro.simplify.intro.apply H.apply inj_neg.assumption.
+ intro.simplify.unfold Not.intro.apply H.apply inj_neg.assumption.
qed.
theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.