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