Module Vars

closedn n M is true iff M is a (de Bruijn) closed term under n binders

closed0 M is true iff M is a (de Bruijn) closed term

noccurn n M returns true iff Rel n does NOT occur in term M

noccur_between n m M returns true iff Rel p does NOT occur in term M for n <= p < n+m

Checking function for terms containing existential- or meta-variables. The function noccur_with_meta does not consider meta-variables applied to some terms (intended to be its local context) (for existential variables, it is necessarily the case)

exliftn el c lifts c with lifting el

liftn n k c lifts by n indexes above or equal to k in c

lift n c lifts by n the positive indexes in c

Let Γ be a context interleaving declarations x₁:T₁..xn:Tn and definitions y₁:=c₁..yp:=cp in some context Γ₀. Let u₁..un be an instance of Γ, i.e. an instance in Γ₀ of the xi. Then, subst_of_rel_context_instance Γ u₁..un returns the corresponding substitution of Γ, i.e. the appropriate interleaving σ of the u₁..un with the c₁..cp, all of them in Γ₀, so that a derivation Γ₀, Γ, Γ₁|- t:T can be instantiated into a derivation Γ₀, Γ₁ |- t[σ]:T[σ] using substnl σ |Γ₁| t. Note that the instance u₁..un is represented starting with u₁, as if usable in applist while the substitution is represented the other way round, i.e. ending with either u₁ or c₁, as if usable for substl.

Take an index in an instance of a context and returns its index wrt to the full context (e.g. 2 in x:A;y:=b;z:C is 3, i.e. a reference to z)

substnl [a₁;...;an] k c substitutes in parallel a₁,...,an for respectively Rel(k+1),...,Rel(k+n) in c; it relocates accordingly indexes in an,...,a1 and c. In terms of typing, if Γ ⊢ a_n..a₁ : Δ and Γ, Δ, Γ' ⊢ c : T with |Γ'|=k, then Γ, Γ' ⊢ substnl [a₁;...;an] k c : substnl [a₁;...;an] k T.

substl σ c is a short-hand for substnl σ 0 c

substl a c is a short-hand for substnl [a] 0 c

substnl_decl [a₁;...;an] k Ω substitutes in parallel a₁, ..., an for respectively Rel(k+1), ..., Rel(k+n) in Ω; it relocates accordingly indexes in a₁,...,an and c. In terms of typing, if Γ ⊢ a_n..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=k, then Γ, Γ', substnl_decl [a₁;...;an] k Ω ⊢.

substl_decl σ Ω is a short-hand for substnl_decl σ 0 Ω

subst1_decl a Ω is a short-hand for substnl_decl [a] 0 Ω

replace_vars k [(id₁,c₁);...;(idn,cn)] t substitutes Var idj by cj in t.

substn_vars k [id₁;...;idn] t substitutes Var idj by Rel j+k-1 in t. If two names are identical, the one of least index is kept. In terms of typing, if Γ,x_n:U_n,...,x₁:U₁,Γ' ⊢ t:T, together with id_j:T_j and Γ,x_n:U_n,...,x₁:U₁,Γ' ⊢ T_j[id_j+1..id_n:=x_j+1..x_n] ≡ Uj, then Γ\{id₁,...,id_n},x_n:U_n,...,x₁:U₁,Γ' ⊢ substn_vars (|Γ'|+1) [id₁;...;idn] t : substn_vars (|Γ'|+1) [id₁;...;idn] T.

subst_vars [id1;...;idn] t is a short-hand for substn_vars [id1;...;idn] 1 t: it substitutes Var idj by Rel j in t. If two names are identical, the one of least index is kept.

subst_var id t is a short-hand for substn_vars [id] 1 t: it substitutes Var id by Rel 1 in t.

Instance substitution for polymorphism.

Ignores the constraints carried by univ_abstracted.