Library GenModelSyntax

Require Import List.
Require Import Models.
Require Import TypeJudge.
Require GenModel.


Module MakeModel (M : CC_Model).

Include GenModel.MakeModel M.
Import T.
Import Term.

Fixpoint int_trm t :=
  match t with
  | Srt prop => T.prop
  | Srt kind => T.kind
  | Ref n => T.Ref n
  | App u v => T.App (int_trm u) (int_trm v)
  | Abs T M => T.Abs (int_trm T) (int_trm M)
  | Prod T U => T.Prod (int_trm T) (int_trm U)
  end.
Definition int_env := List.map int_trm.

Lemma int_lift : forall n t,
  eq_term (int_trm (lift n t)) (T.lift n (int_trm t)).

Lemma int_subst : forall u t,
  eq_term (int_trm (subst u t)) (T.subst (int_trm u) (int_trm t)).

Lemma int_not_kind : forall T, T <> Srt kind -> int_trm (unmark_app T) <> T.kind.

Hint Resolve int_not_kind eq_typ_not_kind.

Lemma int_sound : forall e M M' T,
  eq_typ e M M' T ->
  J.typ (int_env (unmark_env e)) (int_trm (unmark_app M)) (int_trm (unmark_app T)) /\
  J.eq_typ (int_env (unmark_env e)) (int_trm (unmark_app M)) (int_trm (unmark_app M')).


Load "template/Library.v".


  Lemma non_provability : forall T,
    (forall x, ~ el (int_trm (unmark_app T)) vnil x) ->
    forall M M', ~ eq_typ nil M M' T.

End MakeModel.