(** Needs -type-in-type *) Require Import Utf8. Inductive sn {A} (R : A → A → Prop) (x : A) : Prop := | sn_intro : (∀ y : A, R x y → sn R y) → sn R x. Inductive state := | start : state | game {A} (R : A → A → Prop) (Rsn : ∀ x, sn R x) : A → state. Inductive step : state → state → Prop := | step_start {A} (R : A → A → Prop) Rsn x : step start (game R Rsn x) | step_game {A} (R : A → A → Prop) Rsn x y : R x y → step (game R Rsn x) (game R Rsn y). Lemma help_wf A (R : A → A → Prop) Rsn x : sn step (game R Rsn x). Proof. induction (Rsn x) as [x _ IH]; constructor; intros S H; revert H IH. change (step (game R Rsn x) S → match game R Rsn x with | start => True | game R Rsn x => (∀ y, R x y → sn step (game R Rsn y)) → sn step S end); destruct 1; auto. (* manual inversion using match *) Qed. Lemma hypergame_wf S : sn step S. Proof. constructor; destruct 1; auto using help_wf. Qed. Fixpoint infinite (n : nat) : state := match n with | 0 => start | S n => game step hypergame_wf (infinite n) end. Lemma infinite_step n : step (infinite n) (infinite (S n)). Proof. induction n; simpl; constructor; auto. Qed. Lemma hypergame_not_wf : ¬sn step (infinite 0). Proof. intros Hwf; cut (∀ S, sn step S → ∀ n, S ≠ infinite n). { intros help; apply (help _ Hwf 0); auto. } (* strengthen the IH *) induction 1 as [S _ IH]; intros n ->. apply (IH _ (infinite_step n) (S n)); auto. Qed. Definition paradox : False := hypergame_not_wf (hypergame_wf _).