提交 #15

variable (P Q : Nat → Prop)
variable (R : Nat → Nat → Prop)

mutual

inductive A : Nat → Prop
| ca0 : ∀ n, P n → A n
| ca1 : ∀ n1, (∀ n2, R n1 n2 → B n2) → A n1

inductive B : Nat → Prop
| cb0 : ∀ n, Q n → B n
| cb1 : ∀ n1 n2, R n1 n2 → A n2 → B n1
end

theorem neg_a : (∀ n, ¬P n ∧ ¬Q n) → (∀ n₁, ∃ n₂, R n₁ n₂) → (∀ n, A P Q R n → False) := by
  intro h₁ h₂ n a
  refine @A.rec P Q R (λ _ _ ↦ False) (λ _ _ ↦ False) ?_ ?_ ?_ ?_ n a <;> simp [h₁]
  exact λ n _ ↦ h₂ n