fact: Definition fsub x0 n (ts : terms n) x := match le_lt_dec x x0 with | left _ => Var x | right h1 => match le_lt_dec x (x0+n) with | left h2 => Vnth ts (lt_pm h1 h2) | _ => Var x end end.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)