fact: Fixpoint presubst_aux (P: Preterm) (l: nat) (G: Subst) : Preterm := match P with | Fun _ => P | Var i => match (nth_error G i) with | Some (Some Q) => term (lift Q l) | _ => Var i end | App M N => App (presubst_aux M l G) (presubst_aux N l G) | Abs A M => Abs A (presubst_aux M (S l) (None::G) ) end.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)