proposition: Lemma fsub_nil x0 x : fsub x0 Vnil x = Var x.
proof: Proof. unfold fsub. case (le_lt_dec x x0); intro. refl. case (le_lt_dec x (x0+0)); intro. lia. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)