fact: Fixpoint bterm_le k (bt : bterm k) l (h0 : k <= l) : bterm l := match bt with | BVar h => BVar (Nat.le_trans h h0) | BFun f bts => BFun f (Vmap (fun bt => @bterm_le k bt l h0) bts) end.
imports: CoLoR(ATerm VecUtil AInterpretation LogicUtil NatUtil)