``` ```

# Proofs about De Bruijn's Indices

``` Require Import Calculus. Require Import Arith. Require Import MatchCompNat. Require Import Util. Require Import List. Require Import ListSet. Module SetProgram(My_Program: Program). Import My_Program. Require Proofs_Progress. Module My_Proofs_Progress := Proofs_Progress.SetProgram(My_Program). Import My_Proofs_Progress. Import My_Proofs_AdmissibilityOfTransitivity. Import My_Proofs_Subclassing. Import My_Proofs_TypeOrdering. Import My_Proofs_Miscellaneous. Import My_WellFormedness. Import My_Semantics. Import My_Typing. Import My_TypeOrdering. Import My_DeBruijn. Import My_Substitutions. Import My_Subclassing. ```
 Lifting a closed term or type
``` Lemma lemmaA30_0:   forall (p: Path) (n: nat),     (path_is_var_closed p) ->     (lift_in_path p n) = p . ```
 Lifting a closed term or type
``` Lemma lemmaA30_2:   forall (T: type) (n: nat),     (type_is_var_closed T) ->     (lift_in_type T n) = T . ```
 Lifting a closed path
``` Lemma lemmaA30_0':   forall (p: Path) (n k: nat),     (fv_at_depth_in_path p k) = empty_varset ->     (lift_at_depth_in_path p n k) = p . ```
 Lifting a closed type
``` Lemma lemmaA30_2':   forall (T: type) (n k: nat),     (fv_at_depth_in_type T k) = empty_varset ->     (lift_at_depth_in_type T n k) = T . Definition lemmaA30_1_prop1 (t: Term): Prop :=   forall (n k: nat),     (fv_at_depth_in_term t k) = empty_varset ->     (lift_at_depth_in_term t n k) = t . Definition lemmaA30_1_prop2 (fts: FieldTermList): Prop :=   forall (n k: nat),     (fv_at_depth_in_fieldTermList fts k) = empty_varset ->     (lift_at_depth_in_fieldTermList fts n k) = fts . Definition lemmaA30_1_prop3 (xts: ParamTermList): Prop :=   forall (n k: nat),     (fv_at_depth_in_paramTermList xts k) = empty_varset ->     (lift_at_depth_in_paramTermList xts n k) = xts . ```
 Lifting a closed term
``` Lemma lemmaA30_1':   forall (t: Term) (n k: nat),     (fv_at_depth_in_term t k) = empty_varset ->     (lift_at_depth_in_term t n k) = t . ```
 Lifting a closed term
``` Lemma lemmaA30_1:   forall (t: Term) (n: nat),     (term_is_var_closed t) ->     (lift_in_term t n) = t . ```
 Dropping a closed term or type
``` Lemma lemmaA31_0:   forall (p: Path),     (path_is_var_closed p) ->     (drop_in_path p) = p . ```
 Dropping a closed term or type
``` Lemma lemmaA31_2:   forall (T: type),     (type_is_var_closed T) ->     (drop_in_type T) = T . ```
 Dropping a closed path
``` Lemma lemmaA31_0':   forall (p: Path) (k: nat),     (fv_at_depth_in_path p k) = empty_varset ->     (drop_at_depth_in_path p k) = p . ```
 Dropping a closed type
``` Lemma lemmaA31_2':   forall (T: type) (k: nat),     (fv_at_depth_in_type T k) = empty_varset ->     (drop_at_depth_in_type T k) = T . Definition lemmaA31_1_prop1 (t: Term): Prop :=   forall (k: nat),     (fv_at_depth_in_term t k) = empty_varset ->     (drop_at_depth_in_term t k) = t . Definition lemmaA31_1_prop2 (fts: FieldTermList): Prop :=   forall (k: nat),     (fv_at_depth_in_fieldTermList fts k) = empty_varset ->     (drop_at_depth_in_fieldTermList fts k) = fts . Definition lemmaA31_1_prop3 (xts: ParamTermList): Prop :=   forall (k: nat),     (fv_at_depth_in_paramTermList xts k) = empty_varset ->     (drop_at_depth_in_paramTermList xts k) = xts . ```
 Dropping a closed term
``` Lemma lemmaA31_1':   forall (t: Term) (k: nat),     (fv_at_depth_in_term t k) = empty_varset ->     (drop_at_depth_in_term t k) = t . ```
 Dropping a closed term
``` Lemma lemmaA31_1:   forall (t: Term),     (term_is_var_closed t) ->     (drop_in_term t) = t . Definition lemmaA32_prop1 (v: Value): Prop :=   forall (n k: nat),     (lift_at_depth_in_term (value_to_term v) n k) = (value_to_term v) . Definition lemmaA32_prop2 (fvs: FieldValueList): Prop :=   forall (n k: nat),     (lift_at_depth_in_fieldTermList (fieldValueList_to_fieldTermList fvs) n k) =     (fieldValueList_to_fieldTermList fvs) . ```
 Values are invariant by lifting
``` Lemma lemmaA32:   forall (v: Value) (n k: nat),     (lift_at_depth_in_term (value_to_term v) n k) = (value_to_term v) . ```
 Permuting lifting and self substitution
``` ```
 Permuting lifting and self substitution
``` Lemma lemmaA33_0:   forall (p: Path) (n: VarSym) (v: Value),     (lift_in_path (thisSubst_in_path p (Path_value v)) n) =     (thisSubst_in_path (lift_in_path p n) (Path_value v)) . ```
 Permuting lifting and self substitution
``` Lemma lemmaA33_2:   forall (T: type) (n: VarSym) (v: Value),     (lift_in_type (thisSubst_in_type T (Path_value v)) n) =     (thisSubst_in_type (lift_in_type T n) (Path_value v)) . ```
 Permuting lifting and self substitution
``` Lemma lemmaA33_0':   forall (p: Path) (n k: nat) (v: Value),     (lift_at_depth_in_path (thisSubst_in_path p (Path_value v)) n k) =     (thisSubst_in_path (lift_at_depth_in_path p n k) (Path_value v)) . ```
 Permuting lifting and self substitution
``` Lemma lemmaA33_2':   forall (T: type) (n k: nat) (v: Value),     (lift_at_depth_in_type (thisSubst_in_type T (Path_value v)) n k) =     (thisSubst_in_type (lift_at_depth_in_type T n k) (Path_value v)) . Definition lemmaA33_1_prop1 (t: Term): Prop :=   forall (n k: nat) (v: Value),     (lift_at_depth_in_term (thisSubst_in_term t (Path_value v)) n k) =     (thisSubst_in_term (lift_at_depth_in_term t n k) (Path_value v)) . Definition lemmaA33_1_prop2 (fts: FieldTermList): Prop :=   forall (n k: nat) (v: Value),     (lift_at_depth_in_fieldTermList (thisSubst_in_fieldTermList fts (Path_value v)) n k) =     (thisSubst_in_fieldTermList (lift_at_depth_in_fieldTermList fts n k) (Path_value v)) . Definition lemmaA33_1_prop3 (xts: ParamTermList): Prop :=   forall (n k: nat) (v: Value),     (lift_at_depth_in_paramTermList (thisSubst_in_paramTermList xts (Path_value v)) n k) =     (thisSubst_in_paramTermList (lift_at_depth_in_paramTermList xts n k) (Path_value v)) . Lemma lemmaA33_1':   forall (t: Term) (n k: nat) (v: Value),     (lift_at_depth_in_term (thisSubst_in_term t (Path_value v)) n k) =     (thisSubst_in_term (lift_at_depth_in_term t n k) (Path_value v)) . ```
 Permuting lifting and self substitutions
``` Lemma lemmaA33_1:   forall (t: Term) (n: nat) (v: Value),     (lift_in_term (thisSubst_in_term t (Path_value v)) n) =     (thisSubst_in_term (lift_in_term t n) (Path_value v)) . ```
 Permuting lifting and variable substitution
``` Lemma lemmaA35_0':   forall (p: Path) (n k k': VarSym) (v: Value),     (k' <= k) ->     (lift_at_depth_in_path (varSubst_in_path p k v) n k') =     (varSubst_in_path (lift_at_depth_in_path p n k') (k + n) v) . ```
 Permuting lifting and variable substitution
``` Lemma lemmaA35_0:   forall (p: Path) (n k: VarSym) (v: Value),     (lift_in_path (varSubst_in_path p k v) n) =     (varSubst_in_path (lift_in_path p n) (k + n) v) . Lemma lemmaA35_2':   forall (T: type) (n k k': nat) (v: Value),     (k' <= k) ->     (lift_at_depth_in_type (varSubst_in_type T k v) n k') =     (varSubst_in_type (lift_at_depth_in_type T n k') (k + n) v) . ```
 Permuting lifting and variable substitution
``` Lemma lemmaA35_2:   forall (T: type) (n k: VarSym) (v: Value),     (lift_in_type (varSubst_in_type T k v) n) =     (varSubst_in_type (lift_in_type T n) (k + n) v) . Definition lemmaA35_1_prop1 (n: nat) (v: Value) (t: Term): Prop :=   forall (k k': VarSym),     (k' <= k) ->     (lift_at_depth_in_term (varSubst_in_term t k v) n k') =     (varSubst_in_term (lift_at_depth_in_term t n k') (k + n) v) . Definition lemmaA35_1_prop2 (n: nat) (v: Value) (fts: FieldTermList): Prop :=   forall (k k': VarSym),     (k' <= k) ->     (lift_at_depth_in_fieldTermList (varSubst_in_fieldTermList fts k v) n k') =     (varSubst_in_fieldTermList (lift_at_depth_in_fieldTermList fts n k') (k + n) v) . Definition lemmaA35_1_prop3 (n: nat) (v: Value) (xts: ParamTermList): Prop :=   forall (k k': VarSym),     (k' <= k) ->     (lift_at_depth_in_paramTermList (varSubst_in_paramTermList xts k v) n k') =     (varSubst_in_paramTermList (lift_at_depth_in_paramTermList xts n k') (k + n) v) . Lemma lemmaA35_1':   forall (t: Term) (n k k': nat) (v: Value),     (k' <= k) ->     (lift_at_depth_in_term (varSubst_in_term t k v) n k') =     (varSubst_in_term (lift_at_depth_in_term t n k') (k + n) v) . ```
 Permuting lifting and variable substitutions
``` Lemma lemmaA35_1:   forall (t: Term) (n k: VarSym) (v: Value),     (lift_in_term (varSubst_in_term t k v) n) =     (varSubst_in_term (lift_in_term t n) (k + n) v) . ```
 Permuting lifting and parameter substitution
``` ```
 Permuting lifting and parameter substitution
``` Lemma lemmaA34_0':   forall (p: Path) (n k: VarSym) (xvs: list (ParamSym * Value)),     (lift_at_depth_in_path (map_paramSubst_in_path p xvs) n k) =     (map_paramSubst_in_path (lift_at_depth_in_path p n k) xvs) . ```
 Permuting lifting and parameter substitution
``` Lemma lemmaA34_0:   forall (p: Path) (n: VarSym) (xvs: list (ParamSym * Value)),     (lift_in_path (map_paramSubst_in_path p xvs) n) =     (map_paramSubst_in_path (lift_in_path p n) xvs) . ```
 Permuting lifting and parameter substitution
``` Lemma lemmaA34_2':   forall (T: type) (n k: VarSym) (xvs: list (ParamSym * Value)),     (lift_at_depth_in_type (map_paramSubst_in_type T xvs) n k) =     (map_paramSubst_in_type (lift_at_depth_in_type T n k) xvs) . ```
 Permuting lifting and parameter substitution
``` Lemma lemmaA34_2:   forall (T: type) (n: VarSym) (xvs: list (ParamSym * Value)),     (lift_in_type (map_paramSubst_in_type T xvs) n) =     (map_paramSubst_in_type (lift_in_type T n) xvs) . Definition lemmaA34_1_prop1 (n: nat) (xvs: list (ParamSym * Value)) (t: Term): Prop :=   forall (k: nat) ,     (lift_at_depth_in_term (map_paramSubst_in_term t xvs) n k) =     (map_paramSubst_in_term (lift_at_depth_in_term t n k) xvs) . Definition lemmaA34_1_prop2 (n: nat) (xvs: list (ParamSym * Value)) (fts: FieldTermList): Prop :=   forall (k: nat) ,     (lift_at_depth_in_fieldTermList (map_paramSubst_in_fieldTermList fts xvs) n k) =     (map_paramSubst_in_fieldTermList (lift_at_depth_in_fieldTermList fts n k) xvs) . Definition lemmaA34_1_prop3 (n: nat) (xvs: list (ParamSym * Value)) (xts: ParamTermList): Prop :=   forall (k: nat) ,     (lift_at_depth_in_paramTermList (map_paramSubst_in_paramTermList xts xvs) n k) =     (map_paramSubst_in_paramTermList (lift_at_depth_in_paramTermList xts n k) xvs) . Lemma lemmaA34_1':   forall (t: Term) (n k: nat) (xvs: (list (ParamSym * Value))),     (lift_at_depth_in_term (map_paramSubst_in_term t xvs) n k) =     (map_paramSubst_in_term (lift_at_depth_in_term t n k) xvs) . ```
 Permuting lifting and self substitutions
``` Lemma lemmaA34_1:   forall (t: Term) (n: nat) (xvs: (list (ParamSym * Value))),     (lift_in_term (map_paramSubst_in_term t xvs) n) =     (map_paramSubst_in_term (lift_in_term t n) xvs) . ```
``` ```
``` Lemma lemmaA37_0:   forall (p: Path) (k: nat) (v: Value),     (path_is_var_closed p) ->     (varSubst_in_path p k v) = p . ```
``` Lemma lemmaA37_2:   forall (T: type) (k: nat) (v: Value),     (type_is_var_closed T) ->     (varSubst_in_type T k v) = T . Lemma lemmaA37_0':   forall (p: Path) (k: nat) (v: Value),     (fv_at_depth_in_path p k) = empty_varset ->     (varSubst_in_path p k v) = p . Lemma lemmaA37_2':   forall (T: type) (k: nat) (v: Value),     (fv_at_depth_in_type T k) = empty_varset ->     (varSubst_in_type T k v) = T . Definition lemmaA37_1_prop1 (t: Term): Prop :=   forall (k: nat) (v: Value),     (fv_at_depth_in_term t k) = empty_varset ->     (varSubst_in_term t k v) = t . Definition lemmaA37_1_prop2 (fts: FieldTermList): Prop :=   forall (k: nat) (v: Value),     (fv_at_depth_in_fieldTermList fts k) = empty_varset ->     (varSubst_in_fieldTermList fts k v) = fts . Definition lemmaA37_1_prop3 (xts: ParamTermList): Prop :=   forall (k: nat) (v: Value),     (fv_at_depth_in_paramTermList xts k) = empty_varset ->     (varSubst_in_paramTermList xts k v) = xts . ```
 Lifting a closed term
``` Lemma lemmaA37_1':   forall (t: Term) (k: nat) (v: Value),     (fv_at_depth_in_term t k) = empty_varset ->     (varSubst_in_term t k v) = t . ```
 Facts about variable substitution -- term
``` Lemma lemmaA37_1:   forall (t: Term) (k: nat) (v: Value),     (term_is_var_closed t) ->     (varSubst_in_term t 0 v) = t . Definition lemmaA36_32_prop1 (v: Value): Prop :=   forall (k: nat),     (drop_at_depth_in_term (value_to_term v) k) = (value_to_term v) . Definition lemmaA36_32_prop2 (fvs: FieldValueList): Prop :=   forall (k: nat),     (drop_at_depth_in_fieldTermList (fieldValueList_to_fieldTermList fvs) k) =     (fieldValueList_to_fieldTermList fvs) . ```
 Values are invariant by dropping
``` Lemma lemmaA36_32:   forall (v: Value) (k: nat),     (drop_at_depth_in_term (value_to_term v) k) = (value_to_term v) . ```
 Permuting dropping and self substitution
``` ```
 Permuting dropping and self substitution
``` Lemma lemmaA36_33_0:   forall (p: Path) (v: Value),     (drop_in_path (thisSubst_in_path p (Path_value v))) =     (thisSubst_in_path (drop_in_path p) (Path_value v)) . ```
 Permuting dropping and self substitution
``` Lemma lemmaA36_33_2:   forall (T: type) (v: Value),     (drop_in_type (thisSubst_in_type T (Path_value v))) =     (thisSubst_in_type (drop_in_type T) (Path_value v)) . ```
 Permuting dropping and self substitution
``` Lemma lemmaA36_33_0':   forall (p: Path) (k: nat) (v: Value),     (drop_at_depth_in_path (thisSubst_in_path p (Path_value v)) k) =     (thisSubst_in_path (drop_at_depth_in_path p k) (Path_value v)) . ```
 Permuting dropping and self substitution
``` Lemma lemmaA36_33_2':   forall (T: type) (k: nat) (v: Value),     (drop_at_depth_in_type (thisSubst_in_type T (Path_value v)) k) =     (thisSubst_in_type (drop_at_depth_in_type T k) (Path_value v)) . Definition lemmaA36_33_1_prop1 (t: Term): Prop :=   forall (k: nat) (v: Value),     (drop_at_depth_in_term (thisSubst_in_term t (Path_value v)) k) =     (thisSubst_in_term (drop_at_depth_in_term t k) (Path_value v)) . Definition lemmaA36_33_1_prop2 (fts: FieldTermList): Prop :=   forall (k: nat) (v: Value),     (drop_at_depth_in_fieldTermList (thisSubst_in_fieldTermList fts (Path_value v)) k) =     (thisSubst_in_fieldTermList (drop_at_depth_in_fieldTermList fts k) (Path_value v)) . Definition lemmaA36_33_1_prop3 (xts: ParamTermList): Prop :=   forall (k: nat) (v: Value),     (drop_at_depth_in_paramTermList (thisSubst_in_paramTermList xts (Path_value v)) k) =     (thisSubst_in_paramTermList (drop_at_depth_in_paramTermList xts k) (Path_value v)) . Lemma lemmaA36_33_1':   forall (t: Term) (k: nat) (v: Value),     (drop_at_depth_in_term (thisSubst_in_term t (Path_value v)) k) =     (thisSubst_in_term (drop_at_depth_in_term t k) (Path_value v)) . ```
 Permuting dropping and self substitutions
``` Lemma lemmaA36_33_1:   forall (t: Term) (v: Value),     (drop_in_term (thisSubst_in_term t (Path_value v))) =     (thisSubst_in_term (drop_in_term t) (Path_value v)) . ```
 Permuting dropping and variable substitution
``` Lemma lemmaA36_35_0':   forall (p: Path) (k k': VarSym) (v: Value),     k' <= k ->     ((k' = 0) -> ~(varset_In 0 (fv_in_path p))) ->     (drop_at_depth_in_path (varSubst_in_path p (S k) v) k') =     (varSubst_in_path (drop_at_depth_in_path p k') k v) . ```
 Permuting dropping and variable substitution
``` Lemma lemmaA36_35_0:   forall (p: Path) (k: VarSym) (v: Value),     ~(varset_In 0 (fv_in_path p)) ->     (drop_in_path (varSubst_in_path p (S k) v)) =     (varSubst_in_path (drop_in_path p) k v) . Lemma lemmaA36_35_2':   forall (T: type) (k k': nat) (v: Value),     k' <= k ->     ((k' = 0) -> ~(varset_In 0 (fv_in_type T))) ->     (drop_at_depth_in_type (varSubst_in_type T (S k) v) k') =     (varSubst_in_type (drop_at_depth_in_type T k') k v) . ```
 Permuting dropping and variable substitution
``` Lemma lemmaA36_35_2:   forall (T: type) (k: VarSym) (v: Value),     ~(varset_In 0 (fv_in_type T)) ->     (drop_in_type (varSubst_in_type T (S k) v)) =     (varSubst_in_type (drop_in_type T) k v) . Definition lemmaA36_35_1_prop1 (v: Value) (t: Term): Prop :=   forall (k k': VarSym),     (k' <= k) ->     ((k' = 0) -> ~(varset_In 0 (fv_in_term t))) ->     (drop_at_depth_in_term (varSubst_in_term t (S k) v) k') =     (varSubst_in_term (drop_at_depth_in_term t k') k v) . Definition lemmaA36_35_1_prop2 (v: Value) (fts: FieldTermList): Prop :=   forall (k k': VarSym),     (k' <= k) ->     ((k' = 0) -> ~(varset_In 0 (fv_at_depth_in_fieldTermList fts 0))) ->     (drop_at_depth_in_fieldTermList (varSubst_in_fieldTermList fts (S k) v) k') =     (varSubst_in_fieldTermList (drop_at_depth_in_fieldTermList fts k') k v) . Definition lemmaA36_35_1_prop3 (v: Value) (xts: ParamTermList): Prop :=   forall (k k': VarSym),     (k' <= k) ->     ((k' = 0) -> ~(varset_In 0 (fv_at_depth_in_paramTermList xts 0))) ->     (drop_at_depth_in_paramTermList (varSubst_in_paramTermList xts (S k) v) k') =     (varSubst_in_paramTermList (drop_at_depth_in_paramTermList xts k') k v) . Lemma lemmaA36_35_1':   forall (t: Term) (k k': nat) (v: Value),     (k' <= k) ->     ((k' = 0) -> ~(varset_In 0 (fv_in_term t))) ->     (drop_at_depth_in_term (varSubst_in_term t (S k) v) k') =     (varSubst_in_term (drop_at_depth_in_term t k') k v) . ```
 Permuting dropping and variable substitutions
``` Lemma lemmaA36_35_1:   forall (t: Term) (k: VarSym) (v: Value),     ~(varset_In 0 (fv_in_term t)) ->     (drop_in_term (varSubst_in_term t (S k) v)) =     (varSubst_in_term (drop_in_term t) k v) . ```
 Permuting dropping and parameter substitution
``` ```
 Permuting dropping and parameter substitution
``` Lemma lemmaA36_34_0':   forall (p: Path) (k: VarSym) (xvs: list (ParamSym * Value)),     (drop_at_depth_in_path (map_paramSubst_in_path p xvs) k) =     (map_paramSubst_in_path (drop_at_depth_in_path p k) xvs) . ```
 Permuting dropping and parameter substitution
``` Lemma lemmaA36_34_0:   forall (p: Path) (xvs: list (ParamSym * Value)),     (drop_in_path (map_paramSubst_in_path p xvs)) =     (map_paramSubst_in_path (drop_in_path p) xvs) . ```
 Permuting dropping and parameter substitution
``` Lemma lemmaA36_34_2':   forall (T: type) (k: VarSym) (xvs: list (ParamSym * Value)),     (drop_at_depth_in_type (map_paramSubst_in_type T xvs) k) =     (map_paramSubst_in_type (drop_at_depth_in_type T k) xvs) . ```
 Permuting dropping and parameter substitution
``` Lemma lemmaA36_34_2:   forall (T: type) (xvs: list (ParamSym * Value)),     (drop_in_type (map_paramSubst_in_type T xvs)) =     (map_paramSubst_in_type (drop_in_type T) xvs) . Definition lemmaA36_34_1_prop1 (xvs: list (ParamSym * Value)) (t: Term): Prop :=   forall (k: nat) ,     (drop_at_depth_in_term (map_paramSubst_in_term t xvs) k) =     (map_paramSubst_in_term (drop_at_depth_in_term t k) xvs) . Definition lemmaA36_34_1_prop2 (xvs: list (ParamSym * Value)) (fts: FieldTermList): Prop :=   forall (k: nat) ,     (drop_at_depth_in_fieldTermList (map_paramSubst_in_fieldTermList fts xvs) k) =     (map_paramSubst_in_fieldTermList (drop_at_depth_in_fieldTermList fts k) xvs) . Definition lemmaA36_34_1_prop3 (xvs: list (ParamSym * Value)) (xts: ParamTermList): Prop :=   forall (k: nat) ,     (drop_at_depth_in_paramTermList (map_paramSubst_in_paramTermList xts xvs) k) =     (map_paramSubst_in_paramTermList (drop_at_depth_in_paramTermList xts k) xvs) . Lemma lemmaA36_34_1':   forall (t: Term) (k: nat) (xvs: (list (ParamSym * Value))),     (drop_at_depth_in_term (map_paramSubst_in_term t xvs) k) =     (map_paramSubst_in_term (drop_at_depth_in_term t k) xvs) . ```
 Permuting dropping and self substitutions
``` Lemma lemmaA36_34_1:   forall (t: Term) (xvs: (list (ParamSym * Value))),     (drop_in_term (map_paramSubst_in_term t xvs)) =     (map_paramSubst_in_term (drop_in_term t) xvs) . End SetProgram. ```
Index