proposition: Lemma fsub_sup x0 n (ts : terms n) x : x > x0+n -> fsub x0 ts x = Var x.
proof: Proof. intro. unfold fsub. case (le_lt_dec x x0). auto. intro. case (le_lt_dec x (x0+n)). intro. absurd (x>x0+n); lia. auto. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)