Require Import basic.
Require Import Sublogic.
Require Import Models GenModelSyntax.
Require Import ZF ZFcoc.

Module CCM <: CC_Model.

Definition X := set.
Definition inX : X -> X -> Prop := in_set.
Definition eqX : X -> X -> Prop := eq_set.
Definition eqX_equiv : Equivalence eqX := eq_set_equiv.
Notation "x ∈ y" := (inX x y).
Notation "x == y" := (eqX x y).

Lemma in_ext: Proper (eqX ==> eqX ==> iff) inX.
Definition props : X := props.
Definition app : X -> X -> X := cc_app.
Definition lam : X -> (X -> X) -> X := cc_lam.
Definition prod : X -> (X -> X) -> X := cc_prod.

Definition eq_fun (x:X) (f1 f2:X->X) :=
  ∀ y1 y2, y1 ∈ x -> y1 == y2 -> f1 y1 == f2 y2.

Lemma lam_ext :
  ∀ x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  lam x1 f1 == lam x2 f2.

Lemma app_ext:
  ∀ x1 x2 : X, x1 == x2 ->
  ∀ x3 x4 : X, x3 == x4 ->
  app x1 x3 == app x2 x4.
Lemma prod_ext :
  ∀ x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  prod x1 f1 == prod x2 f2.

Lemma prod_intro : ∀ dom f F,
  eq_fun dom f f ->
  eq_fun dom F F ->
  (∀ x, x ∈ dom -> f x ∈ F x) ->
  lam dom f ∈ prod dom F.
Lemma prod_elim : ∀ dom f x F,
  eq_fun dom F F ->
  f ∈ prod dom F ->
  x ∈ dom ->
  app f x ∈ F x.
Lemma impredicative_prod : ∀ dom F,
  eq_fun dom F F ->
  (∀ x, x ∈ dom -> F x ∈ props) ->
  prod dom F ∈ props.
Lemma beta_eq:
  ∀ dom F x,
  eq_fun dom F F ->
  x ∈ dom ->
  app (lam dom F) x == F x.
End CCM.

Module BuildModel := MakeModel(CCM).

Require Import Term Env.
Require Import TypeJudge.
Load "template/Library.v".

Lemma cc_consistency : ∀ M M', ~ eq_typ nil M M' FALSE.