fact: Fixpoint subs s (t : Te) := match t with | Def.Var x => s x | Fun f => t | App u v => App (subs s u) (subs s v) | Lam x u => let x' := var x u s in Lam x' (subs (update x (Var x') s) u) end.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)