Library FType

Require Import List.
Require Import Utf8.
Require Import StdNotations.
Require Import Fix.
Require Import Omega.

Section FType.

  Hypothesis T : Type.
  Hypothesis t0 : T.
  Hypothesis AllT : list T.
  Hypothesis FinT : ∀ x : T, In x AllT.

  Lemma indT : ∀ P, (∀ x, In x AllT → P x) → ∀ x, P x.

  Lemma invT : ∀ P, (∀ x, P x) → (∀ x, In x AllT → P x).

  Section Max.

    Require Import Max.

    Hypothesis P : nat → T → Prop.
    Hypothesis P_all : ∀ r, ∃ n, P n r .
    Hypothesis P_mon : ∀ n n', n ≤ n' → P n ⊆ P n'.

    Inductive forallP : list T → nat → Prop :=
    | forallNil : ∀ n r, P n r → forallP (r::nil) n
    | forallCons : ∀ r n l n', P n r → forallP l n' → forallP (r::l) (max n n').

    Lemma forallP_ex : ∀ l, l ≠ nil → ∃ n, forallP l n.

    Lemma forallP_mon : ∀ l n, forallP l n → ∀ n', n ≤ n' → forallP l n'.

    Lemma ex_swap : ∃ n, ∀ r, P n r.

End Max.

End FType.