proposition: Lemma state_eq_correct s1 s2 : if state_eq s1 s2 then s1 = s2 else s1 <> s2.
proof: Proof. case s1; case s2; intros; unfold state_eq. repeat match goal with |- context[cube_eq ?X ?Y] => generalize (cube_eq_correct X Y); case cube_eq; [idtac | intros HH HH1; case HH; injection HH1; auto]; intros; subst Y end; simpl; auto. repeat match goal with |- context[oeq ?X ?Y] => generalize (oeq_correct X Y); case oeq; [idtac | intros HH HH1; case HH; injection HH1; auto]; intros; subst Y end; simpl; auto. Qed.
imports: ZArith List