Library ZFecc

Require Import ZF ZFpairs ZFnats ZFgrothendieck.
Require Import ZFrelations ZFcoc.

Axiom gr : grothendieck.

Fixpoint ecc (n:nat) : set :=
  match n with
  | 0 => grot_succ props
  | S k => grot_succ (ecc k)
  end.

Lemma ecc_grot : n, grot_univ (ecc n).

Lemma ecc_in1 : n, props ecc n.

Lemma ecc_in2 : n, ecc n ecc (S n).

Lemma ecc_incl : n x, x ecc n -> x ecc (S n).

Lemma ecc_incl_prop : x, x props -> x ecc 0.

Lemma ecc_prod : n X Y,
  ext_fun X Y ->
  X ecc n ->
  ( x, x X -> Y x ecc n) ->
  cc_prod X Y ecc n.

Lemma ecc_prod2 : n X Y,
  ext_fun X Y ->
  X props ->
  ( x, x X -> Y x ecc n) ->
  cc_prod X Y ecc n.