Library GenModelSN
Require Import List Compare_dec.
Require Import Sat.
Require Import Models.
Module Lc := Lambda.
Module Type SN_addon (M : CC_Model).
Import M.
Parameter Red : X -> SAT.
Parameter Red_morph : Proper (eqX ==> eqSAT) Red.
Parameter Red_sort : eqSAT (Red props) snSAT.
Parameter Red_prod : forall A B,
eqSAT (Red (prod A B))
(prodSAT (Red A)
(interSAT (fun p:{y|y\in A} => Red (B (proj1_sig p))))).
Parameter daemon : X.
Parameter daemon_false : daemon \in prod props (fun P => P).
End SN_addon.
Module MakeModel(M : CC_Model) (SN : SN_addon M).
Import M.
Import SN.
Module Xeq.
Definition t := X.
Definition eq := eqX.
Definition eq_equiv : Equivalence eq := eqX_equiv.
End Xeq.
Require Import VarMap.
Module V := VarMap.Make(Xeq).
Notation val := V.map.
Notation eq_val := V.eq_map.
Instance eq_val_equiv : Equivalence eq_val.
Definition vnil : val := V.nil props.
Import V.
Module LCeq.
Definition t := Lc.term.
Definition eq := @Logic.eq Lc.term.
Definition eq_equiv : Equivalence eq := eq_equivalence.
End LCeq.
Module I := VarMap.Make(LCeq).
Notation intt := I.map.
Notation eq_intt := I.eq_map.
Instance eq_intt_equiv : Equivalence eq_intt.
Import I.
Definition ilift (j:intt) : intt :=
fun k => match k with
| 0 => Lc.Ref 0
| S n => Lc.lift 1 (j n)
end.
Instance ilift_morph : Proper (eq_intt ==> eq_intt) ilift.
Qed.
Lemma ilift_lams : forall k f j,
(forall j j', (forall a, Lc.lift 1 (j a) = j' a) ->
forall a, Lc.lift 1 (f j a) = f j' a) ->
eq_intt (ilift (I.lams k f j)) (I.lams (S k) f (ilift j)).
Lemma ilift_binder : forall u j k,
eq_intt
(ilift (fun n => Lc.subst_rec u (j n) k))
(fun n => Lc.subst_rec u (ilift j n) (S k)).
Lemma ilift_binder_lift : forall j k,
eq_intt
(ilift (fun n => Lc.lift_rec 1 (j n) k))
(fun n => Lc.lift_rec 1 (ilift j n) (S k)).
Definition substitutive (t:intt->Lc.term) :=
forall u j k,
t (fun n => Lc.subst_rec u (j n) k) = Lc.subst_rec u (t j) k.
Definition liftable (t:intt->Lc.term) :=
forall j k,
t (fun n => Lc.lift_rec 1 (j n) k) = Lc.lift_rec 1 (t j) k.
Record inftrm := {
iint : val -> X;
iint_morph : Proper (eq_val ==> eqX) iint;
itm : intt -> Lc.term;
itm_morph : Proper (eq_intt ==> @eq Lc.term) itm;
itm_lift : liftable itm;
itm_subst : substitutive itm
}.
Definition trm := option inftrm.
Definition eq_trm (x y:trm) :=
match x, y with
| Some f, Some g =>
(eq_val ==> eqX)%signature (iint f) (iint g) /\
(eq_intt ==> @eq Lc.term)%signature (itm f) (itm g)
| None, None => True
| _, _ => False
end.
Instance eq_trm_refl : Reflexive eq_trm.
Qed.
Instance eq_trm_sym : Symmetric eq_trm.
Qed.
Instance eq_trm_trans : Transitive eq_trm.
Qed.
Instance eq_trm_equiv : Equivalence eq_trm.
Lemma eq_kind : forall (M:trm), M = None <-> eq_trm M None.
Definition tm (j:intt) (M:trm) :=
match M with
| Some f => itm f j
| None => Lc.K
end.
Definition int (i:val) (M:trm) :=
match M with
| Some f => iint f i
| None => props
end.
Lemma eq_trm_intro : forall T T',
(forall i, int i T == int i T') ->
(forall j, tm j T = tm j T') ->
match T, T' with Some _,Some _=>True|None,None=>True|_,_=>False end ->
eq_trm T T'.
Instance tm_morph : Proper (eq_intt ==> eq_trm ==> @eq Lc.term) tm.
Qed.
Lemma tm_substitutive : forall u t j k,
tm (fun n => Lc.subst_rec u (j n) k) t =
Lc.subst_rec u (tm j t) k.
Lemma tm_liftable : forall j t k,
tm (fun n => Lc.lift_rec 1 (j n) k) t = Lc.lift_rec 1 (tm j t) k.
Lemma tm_subst_cons : forall x j t,
tm (I.cons x j) t = Lc.subst x (tm (ilift j) t).
Instance int_morph : Proper (eq_val ==> eq_trm ==> eqX) int.
Qed.
Definition kind : trm := None.
Definition prop : trm.
Defined.
Definition Ref (n:nat) : trm.
Defined.
Definition App (u v:trm) : trm.
Defined.
Definition Abs (A M:trm) : trm.
Defined.
Definition Prod (A B:trm) : trm.
Defined.
Definition lift_rec (n m:nat) (t:trm) : trm.
Defined.
Lemma int_lift_rec_eq : forall n k T i,
int i (lift_rec n k T) == int (V.lams k (V.shift n) i) T.
Definition lift n := lift_rec n 0.
Instance lift_morph : forall k, Proper (eq_trm ==> eq_trm) (lift k).
Qed.
Lemma int_lift_eq : forall i T,
int i (lift 1 T) == int (V.shift 1 i) T.
Lemma int_cons_lift_eq : forall i T x,
int (V.cons x i) (lift 1 T) == int i T.
Lemma tm_lift_rec_eq : forall n k T j,
tm j (lift_rec n k T) = tm (I.lams k (I.shift n) j) T.
Lemma split_lift : forall n T,
eq_trm (lift (S n) T) (lift 1 (lift n T)).
Definition subst_rec (arg:trm) (m:nat) (t:trm) : trm.
Defined.
Lemma int_subst_rec_eq : forall arg k T i,
int i (subst_rec arg k T) == int (V.lams k (V.cons (int (V.shift k i) arg)) i) T.
Definition subst arg := subst_rec arg 0.
Lemma int_subst_eq : forall N M i,
int (V.cons (int i N) i) M == int i (subst N M).
Lemma tm_subst_rec_eq : forall arg k T j,
tm j (subst_rec arg k T) = tm (I.lams k (I.cons (tm (I.shift k j) arg)) j) T.
Lemma tm_subst_eq : forall u v j,
tm j (subst u v) = Lc.subst (tm j u) (tm (ilift j) v).
Instance App_morph : Proper (eq_trm ==> eq_trm ==> eq_trm) App.
Qed.
Instance Abs_morph : Proper (eq_trm ==> eq_trm ==> eq_trm) Abs.
Qed.
Instance Prod_morph : Proper (eq_trm ==> eq_trm ==> eq_trm) Prod.
Qed.
Fixpoint cst_fun (i:val) (e:list trm) (x:X) : X :=
match e with
| List.nil => x
| T::f => lam (int i T) (fun y => cst_fun (V.cons y i) f x)
end.
Instance cst_morph : Proper (eq_val ==> @eq _ ==> eqX ==> eqX) cst_fun.
Qed.
Fixpoint prod_list (e:list trm) (U:trm) :=
match e with
| List.nil => U
| T::f => Prod T (prod_list f U)
end.
Lemma wit_prod : forall x U,
(forall i, x \in int i U) ->
forall e i,
cst_fun i e x \in int i (prod_list e U).
Definition non_empty T :=
exists e, exists2 U, eq_trm T (prod_list e U) &
exists x, forall i, x \in int i U.
Instance non_empty_morph : Proper (eq_trm ==> iff) non_empty.
Qed.
Lemma prop_non_empty : non_empty prop.
Lemma prod_non_empty : forall T U,
non_empty U ->
non_empty (Prod T U).
Lemma non_empty_witness : forall i T,
non_empty T ->
exists x, x \in int i T.
Lemma discr_ref_prod : forall n A B,
~ eq_trm (Ref n) (Prod A B).
Lemma lift1var : forall n, eq_trm (lift 1 (Ref n)) (Ref (S n)).
Lemma non_empty_var_lift : forall n,
non_empty (Ref n) -> non_empty (Ref (S n)).
Definition in_int (i:val) (j:intt) (M T:trm) :=
M <> None /\
match T with
| None => non_empty M
| _ => int i M \in int i T
end /\
inSAT (tm j M) (Red (int i T)).
Instance in_int_morph : Proper
(eq_val ==> pointwise_relation nat (@eq Lc.term) ==> eq_trm ==> eq_trm ==> iff)
in_int.
Qed.
Lemma in_int_not_kind : forall i j M T,
in_int i j M T ->
T <> kind ->
int i M \in int i T /\
inSAT (tm j M) (Red (int i T)).
Lemma in_int_intro : forall i j M T,
int i M \in int i T ->
inSAT (tm j M) (Red (int i T)) ->
M <> kind ->
T <> kind ->
in_int i j M T.
Lemma in_int_var0 : forall i j x t T,
x \in int i T ->
inSAT t (Red (int i T)) ->
T <> kind ->
in_int (V.cons x i) (I.cons t j) (Ref 0) (lift 1 T).
Lemma in_int_varS : forall i j x t n T,
in_int i j (Ref n) (lift (S n) T) ->
in_int (V.cons x i) (I.cons t j) (Ref (S n)) (lift (S (S n)) T).
Lemma in_int_sn : forall i j M T,
in_int i j M T -> Lc.sn (tm j M).
Definition env := list trm.
Definition val_ok (e:env) (i:val) (j:intt) :=
forall n T, nth_error e n = value T ->
in_int i j (Ref n) (lift (S n) T).
Lemma vcons_add_var : forall e T i j x t,
val_ok e i j ->
x \in int i T ->
inSAT t (Red (int i T)) ->
T <> kind ->
val_ok (T::e) (V.cons x i) (I.cons t j).
Lemma add_var_eq_fun : forall T U U' i,
(forall x, x \in int i T -> int (V.cons x i) U == int (V.cons x i) U') ->
eq_fun (int i T)
(fun x => int (V.cons x i) U)
(fun x => int (V.cons x i) U').
Lemma vcons_add_var0 : forall e T i j x,
val_ok e i j ->
x \in int i T ->
T <> kind ->
val_ok (T::e) (V.cons x i) (I.cons daimon j).
Definition wf (e:env) :=
exists i, exists j, val_ok e i j.
Definition typ (e:env) (M T:trm) :=
forall i j, val_ok e i j -> in_int i j M T.
Definition eq_typ (e:env) (M M':trm) :=
forall i j, val_ok e i j -> int i M == int i M'.
Instance typ_morph : forall e, Proper (eq_trm ==> eq_trm ==> iff) (typ e).
Qed.
Instance eq_typ_morph : forall e, Proper (eq_trm ==> eq_trm ==> iff) (eq_typ e).
Qed.
Definition typs e T :=
typ e T kind \/ typ e T prop.
Lemma typs_not_kind : forall e T, wf e -> typs e T -> T <> kind.
Lemma typs_non_empty : forall e T i j,
typs e T ->
val_ok e i j ->
exists x, x \in int i T.
Lemma typ_sn : forall e M T,
wf e -> typ e M T -> exists j, Lc.sn (tm j M).
Lemma wf_nil : wf List.nil.
Lemma wf_cons : forall e T,
wf e ->
typs e T ->
wf (T::e).
Lemma refl : forall e M, eq_typ e M M.
Lemma sym : forall e M M', eq_typ e M M' -> eq_typ e M' M.
Lemma trans : forall e M M' M'', eq_typ e M M' -> eq_typ e M' M'' -> eq_typ e M M''.
Instance eq_typ_setoid : forall e, Equivalence (eq_typ e).
Qed.
Lemma eq_typ_app : forall e M M' N N',
eq_typ e M M' ->
eq_typ e N N' ->
eq_typ e (App M N) (App M' N').
Lemma eq_typ_abs : forall e T T' M M',
eq_typ e T T' ->
eq_typ (T::e) M M' ->
T <> kind ->
eq_typ e (Abs T M) (Abs T' M').
Lemma eq_typ_prod : forall e T T' U U',
eq_typ e T T' ->
eq_typ (T::e) U U' ->
T <> kind ->
eq_typ e (Prod T U) (Prod T' U').
Lemma eq_typ_beta : forall e T M M' N N',
eq_typ (T::e) M M' ->
eq_typ e N N' ->
typ e N T ->
T <> kind ->
eq_typ e (App (Abs T M) N) (subst N' M').
Lemma typ_prop : forall e, typ e prop kind.
Lemma typ_var : forall e n T,
nth_error e n = value T -> typ e (Ref n) (lift (S n) T).
Lemma typ_app : forall e u v V Ur,
typ e v V ->
typ e u (Prod V Ur) ->
V <> kind ->
Ur <> kind ->
typ e (App u v) (subst v Ur).
Lemma typ_abs : forall e T M U,
typs e T ->
typ (T :: e) M U ->
U <> kind ->
typ e (Abs T M) (Prod T U).
Lemma typ_beta : forall e T M N U,
typs e T ->
typ (T::e) M U ->
typ e N T ->
T <> kind ->
U <> kind ->
typ e (App (Abs T M) N) (subst N U).
Lemma typ_prod : forall e T U s2,
s2 = kind \/ s2 = prop ->
typs e T ->
typ (T :: e) U s2 ->
typ e (Prod T U) s2.
Lemma typ_conv : forall e M T T',
typ e M T ->
eq_typ e T T' ->
T <> kind ->
T' <> kind ->
typ e M T'.
End MakeModel.
Require Import Sat.
Require Import Models.
Module Lc := Lambda.
Module Type SN_addon (M : CC_Model).
Import M.
Parameter Red : X -> SAT.
Parameter Red_morph : Proper (eqX ==> eqSAT) Red.
Parameter Red_sort : eqSAT (Red props) snSAT.
Parameter Red_prod : forall A B,
eqSAT (Red (prod A B))
(prodSAT (Red A)
(interSAT (fun p:{y|y\in A} => Red (B (proj1_sig p))))).
Parameter daemon : X.
Parameter daemon_false : daemon \in prod props (fun P => P).
End SN_addon.
Module MakeModel(M : CC_Model) (SN : SN_addon M).
Import M.
Import SN.
Module Xeq.
Definition t := X.
Definition eq := eqX.
Definition eq_equiv : Equivalence eq := eqX_equiv.
End Xeq.
Require Import VarMap.
Module V := VarMap.Make(Xeq).
Notation val := V.map.
Notation eq_val := V.eq_map.
Instance eq_val_equiv : Equivalence eq_val.
Definition vnil : val := V.nil props.
Import V.
Module LCeq.
Definition t := Lc.term.
Definition eq := @Logic.eq Lc.term.
Definition eq_equiv : Equivalence eq := eq_equivalence.
End LCeq.
Module I := VarMap.Make(LCeq).
Notation intt := I.map.
Notation eq_intt := I.eq_map.
Instance eq_intt_equiv : Equivalence eq_intt.
Import I.
Definition ilift (j:intt) : intt :=
fun k => match k with
| 0 => Lc.Ref 0
| S n => Lc.lift 1 (j n)
end.
Instance ilift_morph : Proper (eq_intt ==> eq_intt) ilift.
Qed.
Lemma ilift_lams : forall k f j,
(forall j j', (forall a, Lc.lift 1 (j a) = j' a) ->
forall a, Lc.lift 1 (f j a) = f j' a) ->
eq_intt (ilift (I.lams k f j)) (I.lams (S k) f (ilift j)).
Lemma ilift_binder : forall u j k,
eq_intt
(ilift (fun n => Lc.subst_rec u (j n) k))
(fun n => Lc.subst_rec u (ilift j n) (S k)).
Lemma ilift_binder_lift : forall j k,
eq_intt
(ilift (fun n => Lc.lift_rec 1 (j n) k))
(fun n => Lc.lift_rec 1 (ilift j n) (S k)).
Definition substitutive (t:intt->Lc.term) :=
forall u j k,
t (fun n => Lc.subst_rec u (j n) k) = Lc.subst_rec u (t j) k.
Definition liftable (t:intt->Lc.term) :=
forall j k,
t (fun n => Lc.lift_rec 1 (j n) k) = Lc.lift_rec 1 (t j) k.
Record inftrm := {
iint : val -> X;
iint_morph : Proper (eq_val ==> eqX) iint;
itm : intt -> Lc.term;
itm_morph : Proper (eq_intt ==> @eq Lc.term) itm;
itm_lift : liftable itm;
itm_subst : substitutive itm
}.
Definition trm := option inftrm.
Definition eq_trm (x y:trm) :=
match x, y with
| Some f, Some g =>
(eq_val ==> eqX)%signature (iint f) (iint g) /\
(eq_intt ==> @eq Lc.term)%signature (itm f) (itm g)
| None, None => True
| _, _ => False
end.
Instance eq_trm_refl : Reflexive eq_trm.
Qed.
Instance eq_trm_sym : Symmetric eq_trm.
Qed.
Instance eq_trm_trans : Transitive eq_trm.
Qed.
Instance eq_trm_equiv : Equivalence eq_trm.
Lemma eq_kind : forall (M:trm), M = None <-> eq_trm M None.
Definition tm (j:intt) (M:trm) :=
match M with
| Some f => itm f j
| None => Lc.K
end.
Definition int (i:val) (M:trm) :=
match M with
| Some f => iint f i
| None => props
end.
Lemma eq_trm_intro : forall T T',
(forall i, int i T == int i T') ->
(forall j, tm j T = tm j T') ->
match T, T' with Some _,Some _=>True|None,None=>True|_,_=>False end ->
eq_trm T T'.
Instance tm_morph : Proper (eq_intt ==> eq_trm ==> @eq Lc.term) tm.
Qed.
Lemma tm_substitutive : forall u t j k,
tm (fun n => Lc.subst_rec u (j n) k) t =
Lc.subst_rec u (tm j t) k.
Lemma tm_liftable : forall j t k,
tm (fun n => Lc.lift_rec 1 (j n) k) t = Lc.lift_rec 1 (tm j t) k.
Lemma tm_subst_cons : forall x j t,
tm (I.cons x j) t = Lc.subst x (tm (ilift j) t).
Instance int_morph : Proper (eq_val ==> eq_trm ==> eqX) int.
Qed.
Definition kind : trm := None.
Definition prop : trm.
Defined.
Definition Ref (n:nat) : trm.
Defined.
Definition App (u v:trm) : trm.
Defined.
Definition Abs (A M:trm) : trm.
Defined.
Definition Prod (A B:trm) : trm.
Defined.
Definition lift_rec (n m:nat) (t:trm) : trm.
Defined.
Lemma int_lift_rec_eq : forall n k T i,
int i (lift_rec n k T) == int (V.lams k (V.shift n) i) T.
Definition lift n := lift_rec n 0.
Instance lift_morph : forall k, Proper (eq_trm ==> eq_trm) (lift k).
Qed.
Lemma int_lift_eq : forall i T,
int i (lift 1 T) == int (V.shift 1 i) T.
Lemma int_cons_lift_eq : forall i T x,
int (V.cons x i) (lift 1 T) == int i T.
Lemma tm_lift_rec_eq : forall n k T j,
tm j (lift_rec n k T) = tm (I.lams k (I.shift n) j) T.
Lemma split_lift : forall n T,
eq_trm (lift (S n) T) (lift 1 (lift n T)).
Definition subst_rec (arg:trm) (m:nat) (t:trm) : trm.
Defined.
Lemma int_subst_rec_eq : forall arg k T i,
int i (subst_rec arg k T) == int (V.lams k (V.cons (int (V.shift k i) arg)) i) T.
Definition subst arg := subst_rec arg 0.
Lemma int_subst_eq : forall N M i,
int (V.cons (int i N) i) M == int i (subst N M).
Lemma tm_subst_rec_eq : forall arg k T j,
tm j (subst_rec arg k T) = tm (I.lams k (I.cons (tm (I.shift k j) arg)) j) T.
Lemma tm_subst_eq : forall u v j,
tm j (subst u v) = Lc.subst (tm j u) (tm (ilift j) v).
Instance App_morph : Proper (eq_trm ==> eq_trm ==> eq_trm) App.
Qed.
Instance Abs_morph : Proper (eq_trm ==> eq_trm ==> eq_trm) Abs.
Qed.
Instance Prod_morph : Proper (eq_trm ==> eq_trm ==> eq_trm) Prod.
Qed.
Fixpoint cst_fun (i:val) (e:list trm) (x:X) : X :=
match e with
| List.nil => x
| T::f => lam (int i T) (fun y => cst_fun (V.cons y i) f x)
end.
Instance cst_morph : Proper (eq_val ==> @eq _ ==> eqX ==> eqX) cst_fun.
Qed.
Fixpoint prod_list (e:list trm) (U:trm) :=
match e with
| List.nil => U
| T::f => Prod T (prod_list f U)
end.
Lemma wit_prod : forall x U,
(forall i, x \in int i U) ->
forall e i,
cst_fun i e x \in int i (prod_list e U).
Definition non_empty T :=
exists e, exists2 U, eq_trm T (prod_list e U) &
exists x, forall i, x \in int i U.
Instance non_empty_morph : Proper (eq_trm ==> iff) non_empty.
Qed.
Lemma prop_non_empty : non_empty prop.
Lemma prod_non_empty : forall T U,
non_empty U ->
non_empty (Prod T U).
Lemma non_empty_witness : forall i T,
non_empty T ->
exists x, x \in int i T.
Lemma discr_ref_prod : forall n A B,
~ eq_trm (Ref n) (Prod A B).
Lemma lift1var : forall n, eq_trm (lift 1 (Ref n)) (Ref (S n)).
Lemma non_empty_var_lift : forall n,
non_empty (Ref n) -> non_empty (Ref (S n)).
Definition in_int (i:val) (j:intt) (M T:trm) :=
M <> None /\
match T with
| None => non_empty M
| _ => int i M \in int i T
end /\
inSAT (tm j M) (Red (int i T)).
Instance in_int_morph : Proper
(eq_val ==> pointwise_relation nat (@eq Lc.term) ==> eq_trm ==> eq_trm ==> iff)
in_int.
Qed.
Lemma in_int_not_kind : forall i j M T,
in_int i j M T ->
T <> kind ->
int i M \in int i T /\
inSAT (tm j M) (Red (int i T)).
Lemma in_int_intro : forall i j M T,
int i M \in int i T ->
inSAT (tm j M) (Red (int i T)) ->
M <> kind ->
T <> kind ->
in_int i j M T.
Lemma in_int_var0 : forall i j x t T,
x \in int i T ->
inSAT t (Red (int i T)) ->
T <> kind ->
in_int (V.cons x i) (I.cons t j) (Ref 0) (lift 1 T).
Lemma in_int_varS : forall i j x t n T,
in_int i j (Ref n) (lift (S n) T) ->
in_int (V.cons x i) (I.cons t j) (Ref (S n)) (lift (S (S n)) T).
Lemma in_int_sn : forall i j M T,
in_int i j M T -> Lc.sn (tm j M).
Definition env := list trm.
Definition val_ok (e:env) (i:val) (j:intt) :=
forall n T, nth_error e n = value T ->
in_int i j (Ref n) (lift (S n) T).
Lemma vcons_add_var : forall e T i j x t,
val_ok e i j ->
x \in int i T ->
inSAT t (Red (int i T)) ->
T <> kind ->
val_ok (T::e) (V.cons x i) (I.cons t j).
Lemma add_var_eq_fun : forall T U U' i,
(forall x, x \in int i T -> int (V.cons x i) U == int (V.cons x i) U') ->
eq_fun (int i T)
(fun x => int (V.cons x i) U)
(fun x => int (V.cons x i) U').
Lemma vcons_add_var0 : forall e T i j x,
val_ok e i j ->
x \in int i T ->
T <> kind ->
val_ok (T::e) (V.cons x i) (I.cons daimon j).
Definition wf (e:env) :=
exists i, exists j, val_ok e i j.
Definition typ (e:env) (M T:trm) :=
forall i j, val_ok e i j -> in_int i j M T.
Definition eq_typ (e:env) (M M':trm) :=
forall i j, val_ok e i j -> int i M == int i M'.
Instance typ_morph : forall e, Proper (eq_trm ==> eq_trm ==> iff) (typ e).
Qed.
Instance eq_typ_morph : forall e, Proper (eq_trm ==> eq_trm ==> iff) (eq_typ e).
Qed.
Definition typs e T :=
typ e T kind \/ typ e T prop.
Lemma typs_not_kind : forall e T, wf e -> typs e T -> T <> kind.
Lemma typs_non_empty : forall e T i j,
typs e T ->
val_ok e i j ->
exists x, x \in int i T.
Lemma typ_sn : forall e M T,
wf e -> typ e M T -> exists j, Lc.sn (tm j M).
Lemma wf_nil : wf List.nil.
Lemma wf_cons : forall e T,
wf e ->
typs e T ->
wf (T::e).
Lemma refl : forall e M, eq_typ e M M.
Lemma sym : forall e M M', eq_typ e M M' -> eq_typ e M' M.
Lemma trans : forall e M M' M'', eq_typ e M M' -> eq_typ e M' M'' -> eq_typ e M M''.
Instance eq_typ_setoid : forall e, Equivalence (eq_typ e).
Qed.
Lemma eq_typ_app : forall e M M' N N',
eq_typ e M M' ->
eq_typ e N N' ->
eq_typ e (App M N) (App M' N').
Lemma eq_typ_abs : forall e T T' M M',
eq_typ e T T' ->
eq_typ (T::e) M M' ->
T <> kind ->
eq_typ e (Abs T M) (Abs T' M').
Lemma eq_typ_prod : forall e T T' U U',
eq_typ e T T' ->
eq_typ (T::e) U U' ->
T <> kind ->
eq_typ e (Prod T U) (Prod T' U').
Lemma eq_typ_beta : forall e T M M' N N',
eq_typ (T::e) M M' ->
eq_typ e N N' ->
typ e N T ->
T <> kind ->
eq_typ e (App (Abs T M) N) (subst N' M').
Lemma typ_prop : forall e, typ e prop kind.
Lemma typ_var : forall e n T,
nth_error e n = value T -> typ e (Ref n) (lift (S n) T).
Lemma typ_app : forall e u v V Ur,
typ e v V ->
typ e u (Prod V Ur) ->
V <> kind ->
Ur <> kind ->
typ e (App u v) (subst v Ur).
Lemma typ_abs : forall e T M U,
typs e T ->
typ (T :: e) M U ->
U <> kind ->
typ e (Abs T M) (Prod T U).
Lemma typ_beta : forall e T M N U,
typs e T ->
typ (T::e) M U ->
typ e N T ->
T <> kind ->
U <> kind ->
typ e (App (Abs T M) N) (subst N U).
Lemma typ_prod : forall e T U s2,
s2 = kind \/ s2 = prop ->
typs e T ->
typ (T :: e) U s2 ->
typ e (Prod T U) s2.
Lemma typ_conv : forall e M T T',
typ e M T ->
eq_typ e T T' ->
T <> kind ->
T' <> kind ->
typ e M T'.
End MakeModel.